diff -r 6a753a6d6738 -r c120262044b6 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Wed May 05 14:31:31 1999 +0200
+++ b/doc-src/HOL/HOL.tex	Wed May 05 16:44:42 1999 +0200
@@ -1547,7 +1547,7 @@
 slightly more advanced, though, supporting \emph{extensible record schemes}.
 This admits operations that are polymorphic with respect to record extension,
 yielding ``object-oriented'' effects like (single) inheritance.  See also
-\cite{Naraschewski-Wenzel:1998:TPHOL} for more details on object-oriented
+\cite{NaraschewskiW-TPHOLs98} for more details on object-oriented
 verification and record subtyping in HOL.
 
 
@@ -2763,12 +2763,12 @@
 
 \section{The examples directories}
 
-Directory \texttt{HOL/Auth} contains theories for proving the correctness of 
-cryptographic protocols.  The approach is based upon operational 
-semantics~\cite{paulson-security} rather than the more usual belief logics.
-On the same directory are proofs for some standard examples, such as the 
-Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} 
-and the Otway-Rees protocol.
+Directory \texttt{HOL/Auth} contains theories for proving the correctness of
+cryptographic protocols~\cite{paulson-jcs}.  The approach is based upon
+operational semantics rather than the more usual belief logics.  On the same
+directory are proofs for some standard examples, such as the Needham-Schroeder
+public-key authentication protocol and the Otway-Rees
+protocol.
 
 Directory \texttt{HOL/IMP} contains a formalization of various denotational,
 operational and axiomatic semantics of a simple while-language, the necessary