--- a/Pearl-jv/Paper.thy	Thu Apr 08 00:49:08 2010 -0700
+++ b/Pearl-jv/Paper.thy	Thu Apr 08 10:25:38 2010 +0200
@@ -365,15 +365,13 @@
   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. 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, 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
-  nominal theory as smoothly as possible in Isabelle/HOL, we will follow its
-  characterisation of additive groups.
+  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
+  "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq>  \<pi>\<^sub>2 + \<pi>\<^sub>1"}.  But since the point of this paper is to implement the
+  nominal theory as smoothly as possible in Isabelle/HOL, we tolerate
+  the non-standard notation in order to reuse the existing libraries.
 
   By formalising permutations abstractly as functions, and using a single type
   for all atoms, we can now restate the \emph{permutation properties} from

--- a/Pearl/Paper.thy	Thu Apr 08 00:49:08 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 10:25:38 2010 +0200
@@ -216,12 +216,11 @@
   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:} The main contribution of this paper is in 
+  showing an example of how theorem proving tools can be improved by getting 
+  the right level of abstraction for the underlying theory.
+  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.
@@ -501,7 +500,7 @@
 %text { *
 
   One huge advantage of using bijective permutation functions (as opposed to
-  non-bijective renaming substitutions employed in traditional works syntax) is 
+  non-bijective renaming substitutions employed in traditional works on 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:
@@ -890,10 +889,10 @@
 
   The following Isabelle/HOL command defines a concrete atom type called
   \emph{name}, which consists of atoms whose sort equals the string @{term
-  "''Thy.name''"}.
+  "''name''"}.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"}
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
   \end{isabelle}
 
   \noindent

--- a/Pearl/document/root.tex	Thu Apr 08 00:49:08 2010 -0700
+++ b/Pearl/document/root.tex	Thu Apr 08 10:25:38 2010 +0200
@@ -4,7 +4,6 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{longtable}
 
 
 \usepackage{pdfsetup}