Changeset 726 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (9 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r724 r726  
    102102        false) b c.
    103103
    104 lemma eq_bv_elim: ∀P:bool → Prop. ∀n. ∀x,y.
     104lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
    105105  (x = y → P true) →
    106106  (x ≠ y → P false) →
Note: See TracChangeset for help on using the changeset viewer.