--- a/src/ZF/Bool.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Bool.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/bool.thy
+(* Title: ZF/bool.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Booleans in Zermelo-Fraenkel Set Theory
@@ -10,24 +10,24 @@
Bool = ZF + "simpdata" +
consts
- "1" :: i ("1")
+ "1" :: i ("1")
"2" :: i ("2")
bool :: i
cond :: [i,i,i]=>i
- not :: i=>i
+ not :: i=>i
"and" :: [i,i]=>i (infixl 70)
- or :: [i,i]=>i (infixl 65)
- xor :: [i,i]=>i (infixl 65)
+ 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}"
- cond_def "cond(b,c,d) == if(b=1,c,d)"
- not_def "not(b) == cond(b,0,1)"
- and_def "a and b == cond(a,b,0)"
- or_def "a or b == cond(a,1,b)"
- xor_def "a xor b == cond(a,not(b),b)"
+ bool_def "bool == {0,1}"
+ cond_def "cond(b,c,d) == if(b=1,c,d)"
+ not_def "not(b) == cond(b,0,1)"
+ and_def "a and b == cond(a,b,0)"
+ or_def "a or b == cond(a,1,b)"
+ xor_def "a xor b == cond(a,not(b),b)"
end