doc-src/HOL/HOL.tex
 changeset 6588 6e6ca099f68f parent 6580 ff2c3ffd38ee child 6592 c120262044b6
--- 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$