--- a/Paper/document/root.tex	Fri Jul 23 16:42:00 2010 +0200
+++ b/Paper/document/root.tex	Fri Jul 23 16:42:47 2010 +0200
@@ -75,7 +75,7 @@
 term-constructors where multiple variables are bound at once. Such general
 bindings 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
+extension includes new definitions of $\alpha$-equivalence and establishes
 automatically the reasoning infrastructure for $\alpha$-equated terms. We
 also prove strong induction principles that have the usual variable
 convention already built in.