From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Mar 2012 11:40:06 +0000 (+0000)
Subject: Titols
X-Git-Tag: make_still_working~1880
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e88e55208a612a21e25344df089a77536057bde1

Titols
---

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index be8ddaa59..e0d122934 100644
--- 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 
+(* 
+h1 class="section"Naif Set Theory/h1
+*)
+In this Chapter we shall develop a naif theory of sets represented as 
 characteristic predicates over some universe codeA/code, 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.a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.