--- a/Paper/document/root.tex	Thu Mar 18 19:39:01 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 22:06:28 2010 +0100
@@ -48,13 +48,13 @@
 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 for dealing with general binding structures. Such binding structures
+Isabelle in order to deal with general binding structures. Such binding structures
 are ubiquitous in programming language research and only very poorly supported
-by theorem provers providing only single binding as in the lambda-calculus. We
-give in this paper novel definitions for alpha-equivalence and establish
-automatically the reasoning structure for alpha-equated terms. For example we
-provide a strong induction principle that has the variable convention already
-built in.
+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.
 \end{abstract}