doc-src/HOL/HOL.tex

 Needham-Schroeder public-key authentication protocol~\cite{paulson-ns} 
 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
-equivalence proofs, soundness and completeness of the Hoare rules with respect
-to the 
-denotational semantics, and soundness and completeness of a verification
-condition generator.  Much of development is taken from
+equivalence proofs, soundness and completeness of the Hoare rules with
+respect to the denotational semantics, and soundness and completeness of a
+verification condition generator.  Much of development is taken from
 Winskel~\cite{winskel93}.  For details see~\cite{nipkow-IMP}.
 
 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare
 logic, including a tactic for generating verification-conditions.
 
-Directory \texttt{HOL/MiniML} contains a formalization of the type system of the
-core functional language Mini-ML and a correctness proof for its type
-inference algorithm $\cal W$~\cite{milner78,nazareth-nipkow}.
+Directory \texttt{HOL/MiniML} contains a formalization of the type system of
+the core functional language Mini-ML and a correctness proof for its type
+inference algorithm $\cal W$~\cite{milner78,nipkow-W}.
 
 Directory \texttt{HOL/Lambda} contains a formalization of untyped
 $\lambda$-calculus in de~Bruijn notation and Church-Rosser proofs for $\beta$
 and $\eta$ reduction~\cite{Nipkow-CR}.