Changeset 3103


Ignore:
Timestamp:
Apr 6, 2013, 4:19:18 PM (4 years ago)
Author:
mckinna
Message:

Simplified "include" dependencies

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r3098 r3103  
    1 include "ASM/ASM.ma".
    2 include "ASM/Arithmetic.ma".
    3 include "ASM/Fetch.ma".
    4 include "ASM/Status.ma".
     1
    52include "utilities/extralib.ma".
     3
    64include "ASM/Assembly.ma".
    75
     
    656654  lapply (Hcp_unsafe i Hi) -Hcp_unsafe lapply (Hsafe i Hi) -Hsafe
    657655  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
     656
    658657  [ / by /
    659658  | #x cases x -x #pc #jl #EQ
     
    790789        ]
    791790      ]
     791
    792792qed.
    793793
Note: See TracChangeset for help on using the changeset viewer.