--- 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}"