src/ZF/Bool.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago) changeset 1401 0c439768f45c parent 837 778f01546669 child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax sections
 clasohm@0 1 (* Title: ZF/bool.thy clasohm@0 2 ID: \$Id\$ clasohm@0 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0 4 Copyright 1992 University of Cambridge clasohm@0 5 clasohm@0 6 Booleans in Zermelo-Fraenkel Set Theory lcp@837 7 lcp@837 8 2 is equal to bool, but serves a different purpose clasohm@0 9 *) clasohm@0 10 clasohm@124 11 Bool = ZF + "simpdata" + clasohm@0 12 consts clasohm@1401 13 "1" :: i ("1") clasohm@1401 14 "2" :: i ("2") clasohm@1401 15 bool :: i clasohm@1401 16 cond :: [i,i,i]=>i clasohm@1401 17 not :: i=>i clasohm@1401 18 "and" :: [i,i]=>i (infixl 70) clasohm@1401 19 or :: [i,i]=>i (infixl 65) clasohm@1401 20 xor :: [i,i]=>i (infixl 65) clasohm@0 21 lcp@14 22 translations lcp@14 23 "1" == "succ(0)" lcp@837 24 "2" == "succ(1)" lcp@14 25 lcp@753 26 defs clasohm@0 27 bool_def "bool == {0,1}" clasohm@0 28 cond_def "cond(b,c,d) == if(b=1,c,d)" clasohm@0 29 not_def "not(b) == cond(b,0,1)" clasohm@0 30 and_def "a and b == cond(a,b,0)" clasohm@0 31 or_def "a or b == cond(a,1,b)" clasohm@0 32 xor_def "a xor b == cond(a,not(b),b)" clasohm@0 33 end