src/ZF/Bool.thy
 changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 1629 b5e43a60443a
```     1.1 --- a/src/ZF/Bool.thy	Mon Feb 05 21:33:14 1996 +0100
1.2 +++ b/src/ZF/Bool.thy	Tue Feb 06 12:27:17 1996 +0100
1.3 @@ -1,6 +1,6 @@
1.4 -(*  Title: 	ZF/bool.thy
1.5 +(*  Title:      ZF/bool.thy
1.6      ID:         \$Id\$
1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.9      Copyright   1992  University of Cambridge
1.10
1.11  Booleans in Zermelo-Fraenkel Set Theory
1.12 @@ -10,24 +10,24 @@
1.13
1.14  Bool = ZF + "simpdata" +
1.15  consts
1.16 -    "1"		:: i     	   ("1")
1.17 +    "1"         :: i               ("1")
1.18      "2"         :: i             ("2")
1.19      bool        :: i
1.20      cond        :: [i,i,i]=>i
1.21 -    not		:: i=>i
1.22 +    not         :: i=>i
1.23      "and"       :: [i,i]=>i      (infixl 70)
1.24 -    or		:: [i,i]=>i      (infixl 65)
1.25 -    xor		:: [i,i]=>i      (infixl 65)
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}"
1.35 -    cond_def	"cond(b,c,d) == if(b=1,c,d)"
1.36 -    not_def	"not(b) == cond(b,0,1)"
1.37 -    and_def	"a and b == cond(a,b,0)"
1.38 -    or_def	"a or b == cond(a,1,b)"
1.39 -    xor_def	"a xor b == cond(a,not(b),b)"
1.40 +    bool_def    "bool == {0,1}"
1.41 +    cond_def    "cond(b,c,d) == if(b=1,c,d)"
1.42 +    not_def     "not(b) == cond(b,0,1)"
1.43 +    and_def     "a and b == cond(a,b,0)"
1.44 +    or_def      "a or b == cond(a,1,b)"
1.45 +    xor_def     "a xor b == cond(a,not(b),b)"
1.46  end
```