--- a/doc-src/ZF/ZF.tex Thu May 27 20:49:10 1999 +0200
+++ b/doc-src/ZF/ZF.tex Fri May 28 11:42:07 1999 +0200
@@ -1173,7 +1173,7 @@
These are essential to many definitions that follow, including the natural
numbers and the transitive closure operator. The (co)inductive definition
package also uses the fixedpoint operators~\cite{paulson-CADE}. See
-Davey and Priestley~\cite{davey&priestley} for more on the Knaster-Tarski
+Davey and Priestley~\cite{davey-priestley} for more on the Knaster-Tarski
Theorem and my paper~\cite{paulson-set-II} for discussion of the Isabelle
proofs.