src/ZF/Bool.thy
changeset 837 778f01546669
parent 799 13aa1e3d8a3a
child 1401 0c439768f45c
     1.1 --- a/src/ZF/Bool.thy	Fri Dec 23 16:35:42 1994 +0100
     1.2 +++ b/src/ZF/Bool.thy	Fri Dec 23 16:49:48 1994 +0100
     1.3 @@ -4,20 +4,24 @@
     1.4      Copyright   1992  University of Cambridge
     1.5  
     1.6  Booleans in Zermelo-Fraenkel Set Theory 
     1.7 +
     1.8 +2 is equal to bool, but serves a different purpose
     1.9  *)
    1.10  
    1.11  Bool = ZF + "simpdata" +
    1.12  consts
    1.13 -    "1"		::      "i"     	("1")
    1.14 -    bool        ::      "i"
    1.15 -    cond        ::      "[i,i,i]=>i"
    1.16 -    not		::	"i=>i"
    1.17 -    "and"       ::      "[i,i]=>i"      (infixl 70)
    1.18 -    or		::      "[i,i]=>i"      (infixl 65)
    1.19 -    xor		::      "[i,i]=>i"      (infixl 65)
    1.20 +    "1"		:: "i"     	   ("1")
    1.21 +    "2"         :: "i"             ("2")
    1.22 +    bool        :: "i"
    1.23 +    cond        :: "[i,i,i]=>i"
    1.24 +    not		:: "i=>i"
    1.25 +    "and"       :: "[i,i]=>i"      (infixl 70)
    1.26 +    or		:: "[i,i]=>i"      (infixl 65)
    1.27 +    xor		:: "[i,i]=>i"      (infixl 65)
    1.28  
    1.29  translations
    1.30     "1"  == "succ(0)"
    1.31 +   "2"  == "succ(1)"
    1.32  
    1.33  defs
    1.34      bool_def	"bool == {0,1}"