X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter4.ma;h=aa2f5b08a3fdeb75cf5632f31ed09f80f376b634;hb=be80aa40b9a66d5b12f92d03c2aa7b1dd8e49893;hp=30fae3df079b77fe2bc8d1ce765bc21843b514e4;hpb=770ba48ba232d7f1782629c572820a0f1bfe4fde;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter4.ma b/matita/matita/lib/tutorial/chapter4.ma
index 30fae3df0..aa2f5b08a 100644
--- a/matita/matita/lib/tutorial/chapter4.ma
+++ b/matita/matita/lib/tutorial/chapter4.ma
@@ -280,6 +280,8 @@ To make an example, in the previous case, the unification problem is bool = carr
 and the hint is to take X= mk_DeqSet bool beqb true. The hint is correct, since 
 bool is convertible with (carr (mk_DeqSet bool beb true)). *)
 
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+
 unification hint  0 ≔ ; 
     X ≟ mk_DeqSet bool beqb beqb_true
 (* ---------------------------------------- *) ⊢ 
@@ -334,4 +336,5 @@ unification hint  0 ≔ T1,T2,p1,p2;
 
 example hint2: ∀b1,b2. 
   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
-#b1 #b2 #H @(\P H).
\ No newline at end of file
+#b1 #b2 #H @(\P H).
+qed-.
\ No newline at end of file