--- a/Fun-Paper/document/root.tex	Wed Jun 15 12:32:40 2011 +0100
+++ b/Fun-Paper/document/root.tex	Wed Jun 15 12:52:48 2011 +0100
@@ -36,7 +36,17 @@
 \maketitle
 
 \begin{abstract} 
-bla bla
+Nominal Isabelle provides an infrastructure for formal reasoning about terms
+involving named bound variables. This infrastructure allows bound variables to
+be analysed and manipulated directly. In this way it can mimic informal
+pen-and-pencil reasoning. However, this ability makes defining functions the
+most difficult aspect of the ``nominal approach''.  In this paper we present a
+new way of defining recursive functions over terms with bound variables.  For
+example, we are able to define without difficulties functions for CPS
+translations or the evaluation of lambda-terms, which were previously not
+definable in Nominal Isabelle. We also generalise the
+freshness-condition-for-binders to general binders recently introduced in
+Nominal Isabelle.
 \end{abstract}
 
 \category{CR-number}{subcategory}{third-level}