--- a/src/HOL/IMP/document/root.tex Tue Sep 22 08:38:25 2015 +0200
+++ b/src/HOL/IMP/document/root.tex Tue Sep 22 14:31:22 2015 +0200
@@ -23,6 +23,10 @@
\author{Tobias Nipkow \& Gerwin Klein}
\maketitle
+\begin{abstract}
+This document presents formalizations of the semantics of a simple imperative programming language together with a number of applications: a compiler, type systems, various program analyses and abstract interpreters. These theories form the basis of the book \emph{Concrete Semantics with Isabelle/HOL} by Nipkow and Klein \cite{NipkowK2014}.
+\end{abstract}
+
\setcounter{tocdepth}{2}
\tableofcontents
\newpage