--- a/Pearl-jv/Paper.thy	Sun Apr 11 22:01:56 2010 +0200
+++ b/Pearl-jv/Paper.thy	Sun Apr 11 22:47:45 2010 +0200
@@ -214,15 +214,18 @@
   simple formalisation of the nominal logic work.\smallskip
 
   \noindent
-  {\bf Contributions of the paper:} Our use of a single atom type for representing
-  atoms of different sorts and of functions for representing
-  permutations is not novel, but drastically reduces the number of type classes to just
-  two (permutation types and finitely supported types) that we need in order
-  reason abstractly about properties from the nominal logic work. The novel
-  technical contribution of this paper is a mechanism for dealing with
+  {\bf Contributions of the paper:} Using a single atom type to represent
+  atoms of different sorts and representing permutations as functions are not
+  new ideas.  The main contribution of this paper is to show an example of how
+  to make better theorem proving tools by choosing the right level of
+  abstraction for the underlying theory---our design choices take advantage of
+  Isabelle's type system, type classes, and reasoning infrastructure.
+  The novel
+  technical contribution is a mechanism for dealing with
   ``Church-style'' lambda-terms \cite{Church40} and HOL-based languages
   \cite{PittsHOL4} where variables and variable binding depend on type
   annotations.
+
 *}
 
 section {* Sorted Atoms and Sort-Respecting Permutations *}
@@ -338,7 +341,7 @@
   are \emph{equal}.  We do not have to use the equivalence relation shown
   in~\eqref{permequ} to identify them, as we would if they had been represented
   as lists of pairs.  Another advantage of the function representation is that
-  they form an (additive non-commutative) group provided we define
+  they form a (non-commutative) group provided we define
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -363,9 +366,9 @@
 
   \noindent
   Again this is in contrast to the list-of-pairs representation which does not
-  form a group. The technical importance of this fact is that for groups we
-  can rely on Isabelle/HOL's rich simplification infrastructure.  This will
-  come in handy when we have to do calculations with permutations. 
+  form a group.  The technical importance of this fact is that we can rely on
+  Isabelle/HOL's existing simplification infrastructure for groups, which will
+  come in handy when we have to do calculations with permutations.
   Note that Isabelle/HOL defies standard conventions of mathematical notation
   by using additive syntax even for non-commutative groups.  Obviously,
   composition of permutations is not commutative in general, because @{text
@@ -500,11 +503,13 @@
 
 text {*
 
-  One huge advantage of using bijective permutation functions (as opposed to
-  non-bijective renaming substitutions employed in traditional works syntax) is 
-  the property of \emph{equivariance}
-  and the fact that most HOL-functions (this includes constants) whose argument
-  and result types are permutation types satisfy this property:
+  An \emph{equivariant} function or predicate is one that is invariant under
+  the swapping of atoms.  Having a notion of equivariance with nice logical
+  properties is a major advantage of bijective permutations over traditional
+  renaming substitutions \cite[\S2]{Pitts03}.  Equivariance can be defined
+  uniformly for all permutation types, and it is satisfied by most HOL
+  functions and constants.
+
 
   \begin{definition}\label{equivariance}
   A function @{text f} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> f = f"}.
@@ -741,7 +746,7 @@
   provided @{thm (prem 1) finite_supp_unique[no_vars]},
   @{thm (prem 2) finite_supp_unique[no_vars]}, and for
   all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a}
-  and @{text b} having the same sort, then \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
+  and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}}
   \end{lemma}
 
   \begin{proof}
@@ -1154,9 +1159,9 @@
   user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"}
   where the argument, or arguments, are datatypes for which we can automatically
   define an injective function like @{text "sort_ty"} (see \eqref{sortty}).
-  Our hope is that with this approach Benzmueller and Paulson, the authors of 
-  \cite{PaulsonBenzmueller}, can make headway with formalising their results 
-  about simple type theory.  
+  Our hope is that with this approach Benzmueller and Paulson can make
+  headway with formalising their results
+  about simple type theory \cite{PaulsonBenzmueller}.
   Because of its limitations, they did not attempt this with the old version 
   of Nominal Isabelle. We also hope we can make progress with formalisations of
   HOL-based languages.
@@ -1201,7 +1206,7 @@
   zero to return zero.
 
   We noticed only one disadvantage of the permutations-as-functions: Over
-  lists we can easily perform inductions. For permutation made up from
+  lists we can easily perform inductions. For permutations made up from
   functions, we have to manually derive an appropriate induction principle. We
   can establish such a principle, but we have no real experience yet whether ours
   is the most useful principle: such an induction principle was not needed in