From f1fd103e553c73a3df8c99b66a9a38d471c240a9 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 11:41:23 +0000 Subject: [PATCH] small changes --- weblib/tutorial/chapter4.ma | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) 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}. -- 2.39.2