X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=ff607176483a4ee9159c5264ef7a216393925bcd;hb=eca7393f8b871fd1d7838cfd5a176a80f4ec48c5;hp=20762a99a25975239a42be90d10572eb063c24a1;hpb=d2da1674173236ccb7902490d283741e6de0dd3a;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 20762a99a..ff6071764 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -44,14 +44,17 @@ sets *)
 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
 interpretation "subset" 'subseteq a b = (subset ? a b).
 
-(* Two sets are equals if and only if they have the same elements, that is,
+(* 
+h2 class="section"Set Equality/h2
+Two sets are equals if and only if they have the same elements, that is,
 if the two characteristic functions are extensionally equivalent: *) 
 
 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a a title="iff" href="cic:/fakeuri.def(1)"↔/aspan class="error" title="Parse error: [term] expected after [sym↔] (in [term])"/span Q a.
 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
-(* This notion of equality is different from the intensional equality of
+(*
+This notion of equality is different from the intensional equality of
 functions; the fact it defines an equivalence relation must be explicitly 
 proved: *)
 
@@ -90,7 +93,9 @@ lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
   B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="substraction" href="cic:/fakeuri.def(1)"-/a C.
 #U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/iff_not.def(4)"iff_not/a/span/span/ qed.
 
-(* We can now prove several properties of the previous set-theoretic operations. 
+(* 
+h2 class="section"Simple properties of sets/h2
+We can now prove several properties of the previous set-theoretic operations. 
 In particular, union is commutative and associative, and the empty set is an 
 identity element: *)
 
@@ -225,7 +230,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 
+(* 
+h2 class="section"Unification Hints/h2
+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 +248,7 @@ qed.
 
 definition DeqBool ≝ a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/tutorial/chapter4/beqb.def(2)"beqb/a a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"beqb_true/a.
 
-(* 
-h2 class="section"Unification Hints/h2
-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