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$