- untranslated sections of "formal_topology" commented to make it compile

[helm.git] / matita / matita / lib / tutorial / chapter4.ma

diff --git a/matita/matita/lib/tutorial/chapter4.ma b/matita/matita/lib/tutorial/chapter4.ma
index 30fae3df079b77fe2bc8d1ce765bc21843b514e4..aa2f5b08a3fdeb75cf5632f31ed09f80f376b634 100644 (file)
--- 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