--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/document/root.bib Mon Apr 10 11:33:36 2006 +0200
@@ -0,0 +1,8 @@
+@inproceedings{MehtaN-CADE03,author={Farhad Mehta and Tobias Nipkow},
+title={Proving Pointer Programs in Higher-Order Logic},
+booktitle="Automated Deduction --- CADE-19",editor="F. Baader",
+year=2003,publisher="Springer",series="LNCS",volume={2741},pages={121--135}}
+
+@article{MehtaN-IC05,author={Farhad Mehta and Tobias Nipkow},
+title={Proving Pointer Programs in Higher-Order Logic},
+journal="Information and Computation",year=2005,volume=199,pages={200-227}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/document/root.tex Mon Apr 10 11:33:36 2006 +0200
@@ -0,0 +1,42 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{report}
+\usepackage{graphicx}
+\usepackage[english]{babel}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+\renewcommand{\isamarkupheader}[1]{#1}
+
+\begin{document}
+
+\title{Hoare Logic}
+\author{Various}
+\maketitle
+
+\begin{abstract}
+These theories contain a Hoare logic for a simple imperative
+programming language with while-loops, including a verification
+condition generator.
+
+Special infrastructure for modelling and reasoning about pointer
+programs is provided, together with many examples, including Schorr-Waite.
+See \cite{MehtaN-CADE03,MehtaN-IC05} for an excellent exposition.
+\end{abstract}
+
+\pagestyle{plain}
+\thispagestyle{empty}
+\tableofcontents
+
+\newpage
+
+\input{session}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}