]> matita.cs.unibo.it Git - helm.git/commitdiff
check removed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Dec 2014 11:58:18 +0000 (11:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Dec 2014 11:58:18 +0000 (11:58 +0000)
matita/matita/lib/tutorial/chapter2.ma

index 502e59a40df07f81b67d32e269ea96d613cd2316..1f0244505e3d54333a795f27f16da66ed5686507 100644 (file)
@@ -383,7 +383,7 @@ inductive Pari : nat → Prop ≝
 definition natPari ≝ Sub nat Pari.
 
 definition addPari: natPari → natPari → natPari.
-* #a #Ha * #b #Hb check mk_Sub @(mk_Sub … (add a b))  
+* #a #Ha * #b #Hb @(mk_Sub … (add a b))  
 elim Ha
   [normalize @Hb
   |#x #Hx #Hind normalize @pari2 @Hind