diff -r a6b4d9629b1c -r cdc96d79bbba Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Sat Apr 09 00:28:53 2011 +0100
+++ b/Pearl-jv/Paper.thy	Sat Apr 09 00:29:40 2011 +0100
@@ -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