# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308138768 -3600
# Node ID da6461d8891f7419b55c7f867d5fdaaa63acd0f7
# Parent  e36beb11723c111c0790fe845e23281d779451d1
added an abstract

diff -r e36beb11723c -r da6461d8891f Fun-Paper/document/root.tex
--- 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}