# HG changeset patch
# User lcp
# Date 753705271 -3600
# Node ID bb0caac13effaeac96bbc06d9404235a06954b52
# Parent  c035b6b9eafc727b3713d1f2bc490bcf635c6386
Documents not, and, or, xor: boolean ops

diff -r c035b6b9eafc -r bb0caac13eff doc-src/Logics/ZF.tex
--- a/doc-src/Logics/ZF.tex	Fri Nov 19 11:31:10 1993 +0100
+++ b/doc-src/Logics/ZF.tex	Fri Nov 19 11:34:31 1993 +0100
@@ -1096,6 +1096,10 @@
 \idx{one_def}        1    == succ(0)
 \idx{bool_def}       bool == {0,1}
 \idx{cond_def}       cond(b,c,d) == if(b=1,c,d)
+\idx{not_def}        not(b) == cond(b,0,1)
+\idx{and_def}        a and b == cond(a,b,0)
+\idx{or_def}         a or b == cond(a,1,b)
+\idx{xor_def}        a xor b == cond(a,not(b),b)
 
 \idx{sum_def}        A+B == \{0\}*A Un \{1\}*B
 \idx{Inl_def}        Inl(a) == <0,a>
@@ -1106,7 +1110,7 @@
 \idx{bool_1I}        1 : bool
 \idx{bool_0I}        0 : bool
 
-\idx{boolE}          [| c: bool;  P(1);  P(0) |] ==> P(c)
+\idx{boolE}          [| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P
 \idx{cond_1}         cond(1,c,d) = c
 \idx{cond_0}         cond(0,c,d) = d
 
@@ -1256,9 +1260,9 @@
 and idempotency laws of union and intersection, along with other equations.
 See file \ttindexbold{ZF/equalities.ML}.
 
-Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with a
-conditional operator.  It also defines the disjoint union of two sets, with
-injections and a case analysis operator.  See files
+Figure~\ref{zf-sum} defines $\{0,1\}$ as a set of booleans, with the usual
+operators including a conditional.  It also defines the disjoint union of
+two sets, with injections and a case analysis operator.  See files
 \ttindexbold{ZF/bool.ML} and \ttindexbold{ZF/sum.ML}.
 
 Figure~\ref{zf-qpair} defines a notion of ordered pair that admits