--- a/Pearl-jv/document/root.tex	Tue Mar 01 00:14:02 2011 +0000
+++ b/Pearl-jv/document/root.tex	Wed Mar 02 00:06:28 2011 +0000
@@ -36,12 +36,12 @@
 Pitts et al introduced a beautiful theory about names and 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 make the theory 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 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 extend the nominal logic work with a formalisation of an
+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 
+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.
 \end{abstract}