Changeset 700 for src/ASM/Vector.ma


Ignore:
Timestamp:
Mar 18, 2011, 4:28:26 PM (9 years ago)
Author:
campbell
Message:

Get Clight semantics going again (except for problems CexecEquiv? that I caused
earlier).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r698 r700  
    1212include "arithmetics/nat.ma".
    1313
    14 (* include "oldlib/eq.ma". *)
     14include "utilities/oldlib/eq.ma".
    1515
    1616(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    469469*)
    470470
    471 (* dpm: commented out to get out stuff to typecheck
     471(* dpm: commented out to get out stuff to typecheck *)
    472472lemma eq_v_elim: ∀P:bool → Prop. ∀A,f.
    473473  (∀Q:bool → Prop. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
     
    486486  ]
    487487] qed.
    488 *)
    489488
    490489(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.