--- a/Paper/document/root.tex	Thu Mar 18 23:39:48 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 09:40:34 2010 +0100
@@ -51,7 +51,7 @@
 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
+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
 alpha-equated terms. This includes strong induction principles that have the