Changeset 1516 for src/ASM/Status.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1515 r1516  
    916916  @ le_S_S
    917917  lapply (le_n n)
    918   generalize in ⊢ (?%? → ?(??%?)?)
    919   elim n in ⊢ (∀_:?. ??% → ?(?%??)?)
     918  generalize in ⊢ (?%? → ?(??%?)?);
     919  elim n in ⊢ (∀_:?. ??% → ?(?%??)?);
    920920  [ normalize
    921921    #n
     
    924924    [ //
    925925    | #H #K
    926       inversion K
     926      @(le_inv_ind ?? K …)
    927927      [ # H1
    928928        < H1
     
    946946      # x # K1
    947947      lapply (le_S_S_to_le … K1)
    948       generalize in match m
     948      generalize in match m;
    949949      elim x
    950950      normalize
     
    955955      //
    956956      # q # K2
    957       apply H
     957      @H
    958958      /3/
    959959    ]
Note: See TracChangeset for help on using the changeset viewer.