src/ZF/Bool.thy
 changeset 837 778f01546669 parent 799 13aa1e3d8a3a child 1401 0c439768f45c
```--- a/src/ZF/Bool.thy	Fri Dec 23 16:35:42 1994 +0100
+++ b/src/ZF/Bool.thy	Fri Dec 23 16:49:48 1994 +0100
@@ -4,20 +4,24 @@
Copyright   1992  University of Cambridge

Booleans in Zermelo-Fraenkel Set Theory
+
+2 is equal to bool, but serves a different purpose
*)

Bool = ZF + "simpdata" +
consts
-    "1"		::      "i"     	("1")
-    bool        ::      "i"
-    cond        ::      "[i,i,i]=>i"
-    not		::	"i=>i"
-    "and"       ::      "[i,i]=>i"      (infixl 70)
-    or		::      "[i,i]=>i"      (infixl 65)
-    xor		::      "[i,i]=>i"      (infixl 65)
+    "1"		:: "i"     	   ("1")
+    "2"         :: "i"             ("2")
+    bool        :: "i"
+    cond        :: "[i,i,i]=>i"
+    not		:: "i=>i"
+    "and"       :: "[i,i]=>i"      (infixl 70)
+    or		:: "[i,i]=>i"      (infixl 65)
+    xor		:: "[i,i]=>i"      (infixl 65)

translations
"1"  == "succ(0)"
+   "2"  == "succ(1)"

defs
bool_def	"bool == {0,1}"```