--- a/src/HOL/IMP/document/root.tex Tue Dec 18 21:28:01 2001 +0100
+++ b/src/HOL/IMP/document/root.tex Wed Dec 19 00:26:04 2001 +0100
@@ -1,22 +1,9 @@
\documentclass[a4wide]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-%\usepackage{latexsym}
-%\usepackage{amssymb}
-%\usepackage[english]{babel}
-%\usepackage[latin1]{inputenc}
-%\usepackage[only,bigsqcap]{stmaryrd}
-%\usepackage{wasysym}
-%\usepackage{eufrak}
-
-% this should be the last package used
+\usepackage{graphicx,isabelle,isabellesym}
\usepackage{pdfsetup}
-% proper setup for best-style documents
\urlstyle{rm}
-%\isabellestyle{it}
\renewcommand{\isachardoublequote}{}
% pretty printing for the Com language
@@ -34,28 +21,29 @@
\begin{document}
-\title{IMP--A {\tt WHILE}-language and its Semantics}
-\author{Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, Gerwin Klein}
+\title{IMP --- A {\tt WHILE}-language and its Semantics}
+\author{Gerwin Klein, Heiko Loetzbeyer, Tobias Nipkow, Robert Sandner}
\maketitle
\parindent 0pt\parskip 0.5ex
\begin{abstract}\noindent
-The denotational, operational, and axiomatic semantics, a verification
-condition generator, and all the necessary soundness, completeness and
-equivalence proofs. Essentially a formalization of the first 100 pages
-of \cite{Winskel}.
-
-An eminently readable description of this theory is found in \cite{Nipkow}.
-
-A denotational semantics for IMP based on HOLCF is found in {\tt HOLCF/IMP}.
+ The denotational, operational, and axiomatic semantics, a verification
+ condition generator, and all the necessary soundness, completeness and
+ equivalence proofs. Essentially a formalization of the first 100 pages of
+ \cite{Winskel}.
+
+ An eminently readable description of this theory is found in \cite{Nipkow}.
+ See also HOLCF/IMP for a denotational semantics.
\end{abstract}
\tableofcontents
-\parindent 0pt\parskip 0.5ex
+\begin{center}
+ \includegraphics[scale=0.7]{session_graph}
+\end{center}
-% include generated text of all theories
+\parindent 0pt\parskip 0.5ex
\input{session}
\bibliographystyle{plain}