--- a/Paper/document/root.tex	Mon Oct 04 12:39:57 2010 +0100
+++ b/Paper/document/root.tex	Tue Oct 05 07:30:37 2010 +0100
@@ -69,7 +69,7 @@
 
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
-prover. It provides a proving infrastructure for convenient reasoning about
+prover. It provides a proving infrastructure for reasoning about
 programming language calculi involving named bound variables (as
 opposed to de-Bruijn indices). In this paper we present an extension of
 Nominal Isabelle for dealing with general bindings, that means