doc-src/Logics/ZF.tex

 {\tt FOL} with additional syntax for finite sets, ordered pairs,
 comprehension, general union/intersection, general sums/products, and
 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.
 
 Set theory does not use polymorphism.  All terms in {\ZF} have

 \tdx{Bex_def}            Bex(A,P)  == EX x. x:A & P(x)
 
 \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) ==>
                    b : PrimReplace(A,P) <-> (EX x:A. P(x,b))
 \subcaption{The Zermelo-Fraenkel Axioms}

 \tdx{IntD2}        c : A Int B ==> c : B
 \tdx{IntE}         [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
 
 \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}
 \end{figure}