diff -r a1bb7a7b6205 -r 6e6ca099f68f doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Tue May 04 19:08:58 1999 +0200
+++ b/doc-src/HOL/HOL.tex	Wed May 05 09:43:53 1999 +0200
@@ -2772,18 +2772,17 @@
 
 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$