# HG changeset patch
# User lcp
# Date 788197788 -3600
# Node ID 778f0154666978fdf0b5a0b95645842229a257f0
# Parent  627f4842b0209fed5dc7f8598ab2d64eae5f1d93
Re-indented declarations; declared the number 2

diff -r 627f4842b020 -r 778f01546669 src/ZF/Bool.thy
--- 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}"