Titols

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index be8ddaa594212f9b0dacba4a7d7ddb8c81a23982..e0d122934ef7e49d740beaf498c0ccef2e9f3d9d 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,11 +1,14 @@
-(* In this Chapter we shall develop a naif theory of sets represented as 
+(* 
+\ 5h1 class="section"\ 6Naif Set Theory\ 5/h1\ 6
+*)
+In this Chapter we shall develop a naif theory of sets represented as 
 characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type 
 A→Prop. *)
 
 include "basics/types.ma".
 include "basics/bool.ma".
 
-(**** For instance the empty set is defined by the always function predicate *)
+(* For instance the empty set is defined by the always false function: *)
 
 definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.