commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 20762a99a25975239a42be90d10572eb063c24a1..83a1c28d838598ce34a0eaf5433a28d66b040c45 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -225,7 +225,9 @@ DeqSet is decidable in the traditional sense, namely either a=b or a≠b *)
   [%1 @(\P H) | %2 @(\Pf H)]
 qed.
 
-(* A simple example of a set with a decidable equality is bool. We first define 
+(* 
+\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
+A simple example of a set with a decidable equality is bool. We first define 
 the boolean equality beqb, that is just the xand function, then prove that 
 beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by 
 instantiating the DeqSet record with the previous information *)
@@ -241,9 +243,7 @@ qed.
 
 definition DeqBool ≝ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
 
-(* 
-\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
-At this point, we would expect to be able to prove things like the
+(* At this point, we would expect to be able to prove things like the
 following: for any boolean b, if b==false is true then b=false. 
 Unfortunately, this would not work, unless we declare b of type 
 DeqBool (change the type in the following statement and see what