--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Bool.thy Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,27 @@
+(* Title: ZF/bool.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Booleans in Zermelo-Fraenkel Set Theory
+*)
+
+Bool = ZF +
+consts
+ "1" :: "i" ("1")
+ bool :: "i"
+ cond :: "[i,i,i]=>i"
+ not :: "i=>i"
+ and :: "[i,i]=>i" (infixl 70)
+ or :: "[i,i]=>i" (infixl 65)
+ xor :: "[i,i]=>i" (infixl 65)
+
+rules
+ one_def "1 == succ(0)"
+ 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