Changeset 1516 for src/ASM/Status.ma

Timestamp:

Nov 19, 2011, 12:38:20 AM (8 years ago)

Author:

sacerdot

Message:

Ported to syntax of Matita 0.99.1.

File:

• src/ASM/Status.ma (modified) (4 diffs)

src/ASM/Status.ma

@@ -916 +916 @@
   @ le_S_S
   lapply (le_n n)
-  generalize in ⊢ (?%? → ?(??%?)?)
-  elim n in ⊢ (∀_:?. ??% → ?(?%??)?)
+  generalize in ⊢ (?%? → ?(??%?)?);
+  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
   [ normalize
     #n
@@ -924 +924 @@
     [ //
     | #H #K
-      inversion K
+      @(le_inv_ind ?? K …)
       [ # H1
         < H1
@@ -946 +946 @@
       # x # K1
       lapply (le_S_S_to_le … K1)
-      generalize in match m
+      generalize in match m;
       elim x
       normalize
@@ -955 +955 @@
       //
       # q # K2
-      apply H
+      @H
       /3/
     ]