Changeset 1600 for src/ASM/Status.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/Status.ma

    r1599 r1600  
    66include "ASM/Arithmetic.ma".
    77include "ASM/BitVectorTrie.ma".
    8 include "ASM/JMCoercions.ma".
     8include "basics/russell.ma".
    99
    1010definition Time ≝ nat.
     
    785785
    786786lemma set_arg_16_ok: ∀M,s,v,x. clock M s = clock … (set_arg_16 M s v x).
    787  #M #s #x #v whd in match set_arg_16; normalize nodelta @sig2
     787 #M #s #x #v whd in match set_arg_16; normalize nodelta @pi2
    788788qed.
    789789
     
    926926
    927927lemma set_arg_8_ok: ∀M,s,x,v. clock M s = clock … (set_arg_8 M s x v).
    928  #M #s #x #v whd in match set_arg_8; normalize nodelta @sig2
     928 #M #s #x #v whd in match set_arg_8; normalize nodelta @pi2
    929929qed.
    930930
     
    10841084
    10851085lemma set_arg_1_ok: ∀M,s,x,v. clock M s = clock … (set_arg_1 M s x v).
    1086  #M #s #x #v whd in match set_arg_1; normalize nodelta @sig2
     1086 #M #s #x #v whd in match set_arg_1; normalize nodelta @pi2
    10871087qed.
    10881088
Note: See TracChangeset for help on using the changeset viewer.