src/ZF/Bool.thy

 2 is equal to bool, but serves a different purpose
 *)
 
 Bool = ZF + "simpdata" +
 consts
-    "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)
+    "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)"