--- a/Paper/document/root.tex	Sat Mar 20 18:16:26 2010 +0100
+++ b/Paper/document/root.tex	Sun Mar 21 22:27:08 2010 +0100
@@ -50,13 +50,13 @@
 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 for dealing with general bindings, that means
-term-constructors 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. Our extension includes novel definitions of
-alpha-equivalence and establishes automatically the reasoning infrastructure for
-alpha-equated terms. We can also provide strong induction principles that have 
-the usual variable convention already built in.
+term-constructors 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 lambda-abstractions. Our
+extension includes novel definitions of alpha-equivalence and establishes
+automatically the reasoning infrastructure for alpha-equated terms. We
+also provide strong induction principles that have the usual variable
+convention already built in.
 \end{abstract}