X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter2.ma;h=1f0244505e3d54333a795f27f16da66ed5686507;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=502e59a40df07f81b67d32e269ea96d613cd2316;hpb=b58a13d78f5c7a37000538429aeefcd54662b570;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma
index 502e59a40..1f0244505 100644
--- a/matita/matita/lib/tutorial/chapter2.ma
+++ b/matita/matita/lib/tutorial/chapter2.ma
@@ -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