renamed union_iff to Union_iff
renamed power_set to Pow_iff
DiffD2: now is really a destruction rule

--- a/doc-src/Logics/ZF.tex	Fri Jul 29 13:21:26 1994 +0200
+++ b/doc-src/Logics/ZF.tex	Fri Jul 29 13:28:39 1994 +0200
@@ -126,7 +126,7 @@
 bounded quantifiers.  In most other respects, Isabelle implements precisely
 Zermelo-Fraenkel set theory.
 
-Figure~\ref{zf-constanus} lists the constants and infixes of~\ZF, while
+Figure~\ref{zf-constants} lists the constants and infixes of~\ZF, while
 Figure~\ref{zf-trans} presents the syntax translations.  Finally,
 Figure~\ref{zf-syntax} presents the full grammar for set theory, including
 the constructs of \FOL.
@@ -347,8 +347,8 @@
 \tdx{subset_def}         A <= B  == ALL x:A. x:B
 \tdx{extension}          A = B  <->  A <= B & B <= A
 
-\tdx{union_iff}          A : Union(C) <-> (EX B:C. A:B)
-\tdx{power_set}          A : Pow(B) <-> A <= B
+\tdx{Union_iff}          A : Union(C) <-> (EX B:C. A:B)
+\tdx{Pow_iff}            A : Pow(B) <-> A <= B
 \tdx{foundation}         A=0 | (EX x:A. ALL y:x. ~ y:A)
 
 \tdx{replacement}        (ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
@@ -619,7 +619,7 @@
 
 \tdx{DiffI}        [| c : A;  ~ c : B |] ==> c : A - B
 \tdx{DiffD1}       c : A - B ==> c : A
-\tdx{DiffD2}       [| c : A - B;  c : B |] ==> P
+\tdx{DiffD2}       c : A - B ==> c ~: B
 \tdx{DiffE}        [| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P
 \end{ttbox}
 \caption{Union, intersection, difference} \label{zf-Un}