\documentclass[11pt,a4paper]{report}
\usepackage{graphicx}
\usepackage[english]{babel}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}

\urlstyle{rm}
\isabellestyle{it}

\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}
