Changeset 2121 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 27, 2012, 3:30:58 PM (7 years ago)
Author:
sacerdot
Message:

More functions moved to the places they belong to

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r2006 r2121  
    129129    else
    130130      notb c.
     131
     132lemma eq_b_refl:
     133  ∀b.
     134    eq_b b b = true.
     135  #b cases b //
     136qed.
    131137
    132138lemma eq_b_eq:
Note: See TracChangeset for help on using the changeset viewer.