--- a/Pearl-jv/Paper.thy	Sat Apr 09 13:44:49 2011 +0800
+++ b/Pearl-jv/Paper.thy	Sun Apr 10 04:07:15 2011 +0800
@@ -580,7 +580,7 @@
   variables).  The permutation disappears in cases where the
   constants are equivariant. Given a database of equivariant constants, 
   we can implement a decision procedure that helps to find out when
-  a compound term is equivariant. A permutation @{text \<pi>} can be pushed over
+  a compound term is equivariant. A permutation @{text \<pi>} can be pushed into
   applications and abstractions in a HOL-term as follows
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
@@ -616,7 +616,7 @@
 
   \noindent
   By a meta-argument, that means one we cannot formalise inside
-  Isabelle/HOL, we can convince ourselves that the rewriting process
+  Isabelle/HOL, we can convince ourselves that the strategy of 
   of first pushing a permutation inside a term using
   \eqref{rewriteapplam}, then removing permutation in front of bound
   variables using \eqref{rewriteunpermute} and finally removing all