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