--- a/Pearl-jv/Paper.thy	Thu Apr 08 09:13:36 2010 +0200
+++ b/Pearl-jv/Paper.thy	Thu Apr 08 10:25:13 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