Changeset 1339 for src/common


Ignore:
Timestamp:
Oct 10, 2011, 4:10:32 PM (8 years ago)
Author:
sacerdot
Message:

Automation is now stronger.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r1213 r1339  
    11861186lemma zero_ext_lessdef:
    11871187  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
    1188 #n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
     1188#n #v1 #v2 #H inversion H //
    11891189qed.
    11901190
    11911191lemma sign_ext_lessdef:
    11921192  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
    1193 #n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
     1193#n #v1 #v2 #H inversion H //
    11941194qed.
    11951195(*
Note: See TracChangeset for help on using the changeset viewer.