--- a/Pearl-jv/Paper.thy	Wed May 05 10:24:54 2010 +0100
+++ b/Pearl-jv/Paper.thy	Wed May 05 20:39:21 2010 +0100
@@ -44,30 +44,23 @@
 section {* Introduction *}
 
 text {*
-  The purpose of Nominal Isabelle is to provide a proving infratructure
-  for conveninet reasoning about programming languages. At its core
-  Nominal Isabelle is based on nominal logic by Pitts at al
-  \cite{GabbayPitts02,Pitts03}.  
- 
-  Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
-  prover providing a proving infrastructure for convenient reasoning about
-  programming languages. At its core Nominal Isabelle is based on the nominal
-  logic work of Pitts et al \cite{GabbayPitts02,Pitts03}.  The most basic
-  notion in this work is a sort-respecting permutation operation defined over
-  a countably infinite collection of sorted atoms. The atoms are used for
-  representing variables that might be bound. Multiple sorts are necessary for
-  being able to represent different kinds of variables. For example, in the
-  language Mini-ML there are bound term variables and bound type variables;
-  each kind needs to be represented by a different sort of atoms.
-
+  Nominal Isabelle provides a proving infratructure for
+  convenient reasoning about programming languages. At its core Nominal
+  Isabelle is based on the nominal logic work by Pitts at al
+  \cite{GabbayPitts02,Pitts03}. The most basic notion in this work
+  is a sort-respecting permutation operation defined over a countably infinite
+  collection of sorted atoms. The atoms are used for representing variables
+  that might be bound. Multiple sorts are necessary for being able to
+  represent different kinds of variables. For example, in the language Mini-ML
+  there are bound term variables and bound type variables; each kind needs to
+  be represented by a different sort of atoms.
 
   Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
   atoms and sorts are used in the original formulation of the nominal logic work.
-  Therefore it was decided in earlier versions of Nominal Isabelle to use a
-  separate type for each sort of atoms and let the type system enforce the
-  sort-respecting property of permutations. Inspired by the work on nominal
-  unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
-  implement permutations concretely as lists of pairs of atoms. Thus Nominal
+  The reason is that one has to ensure that permutations are sort-respecting.
+  This was done implicitly in the original nominal logic work \cite{Pitts03}.
+
+
   Isabelle used the two-place permutation operation with the generic type
 
   @{text [display,indent=10] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
@@ -225,6 +218,13 @@
   \cite{PittsHOL4} where variables and variable binding depend on type
   annotations.
 
+   Therefore it was decided in earlier versions of Nominal Isabelle to use a
+  separate type for each sort of atoms and let the type system enforce the
+  sort-respecting property of permutations. Inspired by the work on nominal
+  unification \cite{UrbanPittsGabbay04}, it seemed best at the time to also
+  implement permutations concretely as lists of pairs of atoms.
+
+
 *}
 
 section {* Sorted Atoms and Sort-Respecting Permutations *}

--- 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