Changeset 961 for src/ASM/BitVector.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r868 r961 110 110 #Q * *; normalize /3/ 111 111 qed. 112 113 lemma eq_bv_true: ∀n,v. eq_bv n v v = true. 114 @eq_v_true * @refl 115 qed. 116 117 lemma eq_bv_false: ∀n,v,v'. v ≠ v' → eq_bv n v v' = false. 118 #n #v #v' #NE @eq_v_false [ * * #H try @refl normalize in H; destruct  @NE ] 119 qed. 112 120 113 121 axiom bitvector_of_string:
Note: See TracChangeset
for help on using the changeset viewer.