summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 05 May 1999 09:43:53 +0200 | |

changeset 6588 | 6e6ca099f68f |

parent 6587 | a1bb7a7b6205 |

child 6589 | 41b44b20a1b4 |

Bibtex stuff.

doc-src/HOL/HOL.tex | file | annotate | diff | comparison | revisions | |

doc-src/HOL/logics-HOL.tex | file | annotate | diff | comparison | revisions |

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

--- a/doc-src/HOL/logics-HOL.tex Tue May 04 19:08:58 1999 +0200 +++ b/doc-src/HOL/logics-HOL.tex Wed May 05 09:43:53 1999 +0200 @@ -56,6 +56,7 @@ \include{../Logics/syntax} \include{HOL} \bibliographystyle{plain} -\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} +\bibliography{../isabelle} +%\bibliography{string,general,atp,theory,funprog,logicprog,isabelle,crossref} \input{logics-HOL.ind} \end{document}