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}.
@@ -2386,10 +2386,10 @@
 \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