--- 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