--- a/Pearl-jv/document/root.tex	Mon May 03 08:52:15 2010 +0100
+++ b/Pearl-jv/document/root.tex	Tue May 04 05:36:43 2010 +0100
@@ -24,28 +24,21 @@
 
 \begin{document}
 
-\title{Proof Pearl: A New Foundation for Nominal Isabelle}
+\title{Implementing the Nominal Logic Work in Isabelle/HOL}
 \author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
 \institute{Portland State University \and Technical University of Munich}
 \maketitle
 
 \begin{abstract}
 Pitts et al introduced a beautiful theory about names and binding based on the
-notions of permutation 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 differs from our earlier approach
-in two important respects: First, instead of representing permutations as
-lists of pairs of atoms, we now use a more abstract representation based on
-functions.  Second, whereas the earlier work modeled different sorts of atoms
-using different types, we now introduce a unified atom type that includes all
-sorts of atoms. Interestingly, we allow swappings, that is permutations build from
-two atoms, to be ill-sorted.  As a result of these design changes, we can iron
-out inconveniences for the user, considerably simplify proofs and also
-drastically reduce the amount of custom ML-code. Furthermore we can extend the
-capabilities of Nominal Isabelle to deal with variables that carry additional
-information. We end up with a pleasing and formalised theory of permutations
-and support, on which we can build an improved and more powerful version of
-Nominal Isabelle.
+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.
 \end{abstract}
 
 % generated text of all theories