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