--- a/Pearl-jv/document/root.tex	Wed May 05 10:24:54 2010 +0100
+++ b/Pearl-jv/document/root.tex	Wed May 05 20:39:21 2010 +0100
@@ -31,14 +31,13 @@
 
 \begin{abstract}
 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
+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.  We present a formalisation of this work that is based on a
-unified atom type (that includes all sorts of atoms) 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.  Furthermore we can extend the nominal logic with names that carry
-additional information.
+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.  Furthermore we extend the nominal
+logic work with names that carry additional information.
 \end{abstract}
 
 % generated text of all theories