Changeset 1600 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:41:08 PM (8 years ago)
Author:
sacerdot
Message:

utilities and ASM ported to the new standard library

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1598 r1600  
    22include "ASM/Arithmetic.ma".
    33include "ASM/ASM.ma".
     4include "basics/russell.ma".
    45
    56definition bitvector_max_nat ≝
     
    89
    910definition code_memory_size ≝ bitvector_max_nat 16.
    10 
    11 include "ASM/JMCoercions.ma".
    1211
    1312axiom bitvector_lt_bitvector_max_nat:
Note: See TracChangeset for help on using the changeset viewer.