--- a/Pearl-jv/document/root.tex	Mon Feb 28 15:21:10 2011 +0000
+++ b/Pearl-jv/document/root.tex	Mon Feb 28 16:47:13 2011 +0000
@@ -36,12 +36,13 @@
 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.  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.  Furthermore we extend the nominal
-logic work with names that carry additional information and with a
-formalisation of abstractions that bind finite sets of names.
+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
+abstraction operator that binds sets of names.
 \end{abstract}
 
 % generated text of all theories