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