--- a/Paper/document/root.tex	Fri Mar 19 10:24:49 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 12:31:17 2010 +0100
@@ -39,7 +39,7 @@
 
 \begin{document}
 
-\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to
+\title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to
   Formalise Core-Haskell}
 \maketitle
 
@@ -49,13 +49,14 @@
 prover. It provides a proving infrastructure for convenient reasoning about
 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
+Nominal Isabelle for dealing with general binding structures, that means
+where multiple variables are bound at once. Such
 binding structures are ubiquitous in programming language research and only
 very poorly supported with single binders, such as the lambdas in the
-lambda-calculus. For our extension we introduce novel definitions of
-alpha-equivalence and establish automatically the reasoning infrastructure for
+lambda-calculus. Our extension includes novel definitions of
+alpha-equivalence and establishes automatically the reasoning infrastructure for
 alpha-equated terms. This includes strong induction principles that have the
-variable convention already built in.
+usual variable convention already built in.
 \end{abstract}