src/ZF/Bool.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
--- a/src/ZF/Bool.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Bool.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,10 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Booleans in Zermelo-Fraenkel Set Theory 
+*)
 
-2 is equal to bool, but serves a different purpose
-*)
+header{*Booleans in Zermelo-Fraenkel Set Theory*}
 
 theory Bool = pair:
 
@@ -18,6 +17,8 @@
    "1"  == "succ(0)"
    "2"  == "succ(1)"
 
+text{*2 is equal to bool, but is used as a number rather than a type.*}
+
 constdefs
   bool        :: i
     "bool == {0,1}"