diff -r 4c2e424cb858 -r 6454f5c9d211 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Wed Apr 07 22:08:46 2010 +0200
+++ b/Pearl/Paper.thy	Wed Apr 07 23:39:08 2010 -0700
@@ -337,7 +337,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}
@@ -362,17 +362,15 @@
 
   \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. 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
-  "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.
+  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---@{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