--- a/Pearl-jv/document/root.tex	Wed Mar 02 00:06:28 2011 +0000
+++ b/Pearl-jv/document/root.tex	Tue Mar 08 09:07:27 2011 +0000
@@ -37,12 +37,12 @@
 notions of atoms, permutations and support. The engineering challenge is to
 smoothly adapt this theory to a theorem prover environment, in our case
 Isabelle/HOL. For this we have to formulate the theory so that it is
-compatible with choice principles, which the work by Pitts is not.  We 
-present a formalisation of this work that is based on a unified atom type 
+compatible with HOL, which the original formulation by Pitts is not.  We 
+present a formalisation that is based on a unified atom type 
 and that represents permutations by bijective functions from atoms to atoms. 
 Interestingly, we allow swappings, which are permutations build from two
-atoms, to be ill-sorted.  We also describe a formalisation of an 
-abstraction operator that binds sets of names.
+atoms, to be ill-sorted.  We also describe a formalisation of two 
+abstraction operators that bind sets of names.
 \end{abstract}
 
 % generated text of all theories