--- a/Paper/document/root.tex	Thu Mar 18 23:38:01 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 23:39:26 2010 +0100
@@ -47,14 +47,15 @@
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
-programming language calculi. In this paper we present an extension of Nominal
-Isabelle in order to deal with general binding structures. Such binding structures
-are ubiquitous in programming language research and only very poorly supported
-with single binders, as for example found in the lambda-calculus. For our
-extension we introduce novel definitions of alpha-equivalence and establish
-automatically the reasoning infrastructure for alpha-equated terms. This
-includes a strong induction principle which has the variable convention
-already built in.
+programming language calculi involving bound variables that have names (as
+opposed to de-Bruijn indices). In this paper we present an extension of
+Nominal Isabelle in order to deal with general binding structures. Such
+binding structures are ubiquitous in programming language research and only
+very poorly supported with single binders, as for example found in the
+lambda-calculus. For our extension we introduce novel definitions of
+alpha-equivalence and establish automatically the reasoning infrastructure for
+alpha-equated terms. This includes strong induction principles that have the
+variable convention already built in.
 \end{abstract}