src/HOL/Hoare/document/root.tex

explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)

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