# HG changeset patch
# User nipkow
# Date 1144661616 -7200
# Node ID 17382f02079e0444d100ae377e22d924f889cc75
# Parent  fd2ba98056a2cf3a2dd3c0f03981c4ce2e04550f
Minimal doc

diff -r fd2ba98056a2 -r 17382f02079e src/HOL/Hoare/document/root.bib
--- /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}}
diff -r fd2ba98056a2 -r 17382f02079e src/HOL/Hoare/document/root.tex
--- /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}