summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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$