Changeset 2124 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (8 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r2119 r2124  
    1717  λpc: Word.
    1818    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    19 
    20 (*CSC: move elsewhere *)
    21 axiom eq_bitvector_of_nat_to_eq:
    22  ∀n,n1,n2.
    23   n1 < 2^n → n2 < 2^n →
    24    bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
    25 
    26 discriminator Prod.
    2719
    2820definition load_code_memory0:
Note: See TracChangeset for help on using the changeset viewer.