doc-src/ZF/ZF.tex
 changeset 6592 c120262044b6 parent 6173 2c0579e8e6fa child 6745 74e8f703f5f2
--- a/doc-src/ZF/ZF.tex	Wed May 05 14:31:31 1999 +0200
+++ b/doc-src/ZF/ZF.tex	Wed May 05 16:44:42 1999 +0200
@@ -31,7 +31,7 @@
Published articles~\cite{paulson-set-I,paulson-set-II} describe \texttt{ZF}
less formally than this chapter.  Isabelle employs a novel treatment of
non-well-founded data structures within the standard {\sc zf} axioms including
-the Axiom of Foundation~\cite{paulson-final}.
+the Axiom of Foundation~\cite{paulson-mscs}.

\section{Which version of axiomatic set theory?}
@@ -1116,7 +1116,7 @@
non-standard notion of disjoint sum using non-standard pairs.  All of these
concepts satisfy the same properties as their standard counterparts; in
addition, {\tt<$a$;$b$>} is continuous.  The theory supports coinductive
-definitions, for example of infinite lists~\cite{paulson-final}.
+definitions, for example of infinite lists~\cite{paulson-mscs}.

\begin{figure}
\begin{ttbox}
@@ -2386,10 +2386,10 @@
induction.

\item Theory \texttt{ListN} inductively defines the lists of $n$
-  elements~\cite{paulin92}.
+  elements~\cite{paulin-tlca}.

\item Theory \texttt{Acc} inductively defines the accessible part of a
-  relation~\cite{paulin92}.
+  relation~\cite{paulin-tlca}.

\item Theory \texttt{Comb} defines the datatype of combinators and
inductively defines contraction and parallel contraction.  It goes on to