From: matitaweb Date: Wed, 7 Mar 2012 11:41:23 +0000 (+0000) Subject: small changes X-Git-Tag: make_still_working~1879 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1fd103e553c73a3df8c99b66a9a38d471c240a9;p=helm.git small changes --- 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}.