X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=weblib%2Ftutorial%2Fchapter4.ma;h=ff607176483a4ee9159c5264ef7a216393925bcd;hb=30172d86a0cd979e44ae3343655f6ce55043dd52;hp=83a1c28d838598ce34a0eaf5433a28d66b040c45;hpb=f09ad987d622554030aafe383a4396c95899ec91;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 83a1c28d8..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: *)