diff -r 759b5299a9f2 -r 1a690dce8cfc src/HOL/IMP/document/root.tex
--- 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