\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{isabelle,isabellesym}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{Hoare Logic}
\author{
Norbert Galm \\
Walter Guttmann \\
Farhad Mehta \\
Tobias Nipkow \\
Leonor Prensa Nieto}
\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
\begin{center}
\includegraphics[scale=0.5]{session_graph}
\end{center}
\clearpage
\input{session}
\bibliographystyle{plain}
\bibliography{root}
\end{document}