Changeset 891 for src/common/Values.ma
- Timestamp:
- Jun 7, 2011, 4:53:53 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Values.ma
r797 r891 64 64 | @H2 % #E destruct elim H3 /2/ 65 65 ] qed. 66 67 lemma eq_block_b_b : ∀b. eq_block b b = true. 68 * * #z whd in ⊢ (??%?) >eqZb_z_z @refl 69 qed. 66 70 67 71 (* Characterise the memory regions which the pointer representations can … … 1225 1229 lemma sign_ext_lessdef: 1226 1230 ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2). 1227 #n #v1 #v2 #H inversion H ;//;#v #e1 #e2 <e1 in H >e2 //;1231 #n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) // 1228 1232 qed. 1229 1233 (*
Note: See TracChangeset
for help on using the changeset viewer.