author lcp Fri Dec 23 16:49:48 1994 +0100 (1994-12-23 ago) changeset 837 778f01546669 parent 836 627f4842b020 child 838 120edb26ee93
Re-indented declarations; declared the number 2
 src/ZF/Bool.thy file | annotate | diff | revisions
```     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}"
```