--- a/Pearl/Paper.thy	Wed Apr 07 22:08:46 2010 +0200
+++ b/Pearl/Paper.thy	Thu Apr 08 08:40:49 2010 +0200
@@ -48,7 +48,7 @@
   programming languages. It has been used to formalise an equivalence checking
   algorithm for LF \cite{UrbanCheneyBerghofer08}, 
   Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-  \cite{BengtsonParrow07,BengtsonParow09} and a strong normalisation result for
+  \cite{BengtsonParrow07} and a strong normalisation result for
   cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used
   by Pollack for formalisations in the locally-nameless approach to binding
   \cite{SatoPollack10}.
@@ -218,7 +218,7 @@
   \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 drastically reduces the number of type classes to just
+  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
@@ -242,10 +242,11 @@
 
 text {*
   \noindent
-  whereby the string argument specifies the sort of the atom.  (We use type
-  \emph{string} merely for convenience; any countably infinite type would work
-  as well.)  A similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} 
-  for their variables. 
+  whereby the string argument specifies the sort of the atom.\footnote{A similar 
+  design choice was made by Gunter et al \cite{GunterOsbornPopescu09} 
+  for their variables.}  (The use type
+  \emph{string} is merely for convenience; any countably infinite type would work
+  as well.) 
   We have an auxiliary function @{text sort} that is defined as @{thm
   sort_of.simps[no_vars]}, and we clearly have for every finite set @{text X} of
   atoms and every sort @{text s} the property:
@@ -367,7 +368,7 @@
   come in handy when we have to do calculations with permutations. However,
   note that in this case Isabelle/HOL neglects well-entrenched mathematical
   terminology that associates with an additive group a commutative
-  operation. Obviously, permutations are not commutative in general---@{text
+  operation. Obviously, permutations are not commutative in general, because @{text
   "p + q \<noteq> q + p"}. However, it is quite difficult to work around this
   idiosyncrasy of Isabelle/HOL, unless we develop our own algebraic hierarchy
   and infrastructure. But since the point of this paper is to implement the
@@ -813,11 +814,7 @@
   fresh atom with arbitrary sort. This is an important operation in Nominal
   Isabelle in situations where, for example, a bound variable needs to be
   renamed. To allow such a choice, we only have to assume \emph{one} premise
-  of the form
-
-  @{text [display,indent=10] "finite (supp x)"}
-
-  \noindent
+  of the form @{text "finite (supp x)"}
   for each @{text x}. Compare that with the sequence of premises in our earlier
   version of Nominal Isabelle (see~\eqref{fssequence}). For more convenience we
   can define a type class for types where every element has finite support, and
@@ -926,7 +923,7 @@
   defines an overloaded function that maps from the concrete type into the
   generic atom type, which we will write @{text "|_|"}.  For each class
   instance, this function must be injective and equivariant, and its outputs
-  must all have the same sort.
+  must all have the same sort, that is
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   i)   \hspace{1mm}if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\hspace{4mm}
@@ -1153,8 +1150,8 @@
   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 
+  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.  
   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