X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=b56caaa662df48597fa486de75f507ab324b7d5a;hb=f1fd103e553c73a3df8c99b66a9a38d471c240a9;hp=e0d122934ef7e49d740beaf498c0ccef2e9f3d9d;hpb=e88e55208a612a21e25344df089a77536057bde1;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index e0d122934..b56caaa66 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,14 +1,13 @@
 (* 
 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 false function: *)
+(* 
+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. 
+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}.