Sectionin

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 83a1c28d838598ce34a0eaf5433a28d66b040c45..32a3f23eaa596d83d75f801a7df4047678cea905 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -44,14 +44,16 @@ 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,
+(* \ 5h2 class="section"\ 6Set Quality\ 5/h2\ 6
+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 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 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: *)
 

diff --git a/weblib/tutorial/chapter5.ma b/weblib/tutorial/chapter5.ma
index 014cb611f94cdc7be6eecc41beaa6479f23a2421..f0c4977077a4bd9f789d2d9cf12a230d2f2edaa6 100644 (file)
--- a/weblib/tutorial/chapter5.ma
+++ b/weblib/tutorial/chapter5.ma
@@ -1,4 +1,6 @@
-(* The fact of being able to decide, via a computable boolean function, the 
+(* 
+\ 5h1 class="section"\ 5Effective searching/h1\ 6
+The fact of being able to decide, via a computable boolean function, the 
 equality between elements of a given set is an essential prerequisite for 
 effectively searching an element of that set inside a data structure. In this 
 section we shall define several boolean functions acting on lists of elements in