--- a/Pearl-jv/Paper.thy	Fri Apr 22 00:18:25 2011 +0800
+++ b/Pearl-jv/Paper.thy	Thu Apr 28 11:44:36 2011 +0800
@@ -495,7 +495,7 @@
 
 text {*
   An important notion in the nominal logic work is
-  \emph{equivariance}.  It will enable us to characterise how
+  \emph{equivariance}.  This notion allows us to characterise how
   permutations act upon compound statements in HOL by analysing how
   these statements are constructed.  To do so, let us first define
   \emph{HOL-terms}. They are given by the grammar