--- a/Pearl-jv/Paper.thy	Fri Apr 08 14:23:28 2011 +0800
+++ b/Pearl-jv/Paper.thy	Sat Apr 09 02:10:49 2011 +0800
@@ -68,7 +68,7 @@
   Pitts at al \cite{GabbayPitts02,Pitts03}, whose most basic notion is
   a sort-respecting permutation operation defined over a countably
   infinite collection of sorted atoms. The aim of this paper is to
-  describe how to adapt this work so that it can be implemented in a
+  describe how we adapted this work so that it can be implemented in a
   theorem prover based on Higher-Order Logic (HOL). For this we
   present the definition we made in the implementation and also review
   many proofs. There are a two main design choices to be made. One is