--- a/Pearl-jv/document/root.tex	Mon Mar 14 16:35:59 2011 +0100
+++ b/Pearl-jv/document/root.tex	Tue Mar 15 00:40:39 2011 +0100
@@ -38,9 +38,9 @@
 binding based on the 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 HOL, which the original formulation by
-Pitts is not.  We achieve this by not requiring that every object in our
-discourse has finite support. We present a formalisation that is based on a
+theory so that it is compatible with Higher-Order Logic, which the original formulation by
+Pitts is not.  We achieve this by not requiring that every construction has 
+to have finite support. 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