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