--- a/Nominal/Nominal2_FSet.thy	Thu Apr 08 09:12:13 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Thu Apr 08 09:13:36 2010 +0200
@@ -24,23 +24,13 @@
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
-  by (rule permute_zero)
-
-lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
-  by (lifting permute_list_zero)
-
-lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
-  by (rule permute_plus)
-
-lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
-  by (lifting permute_list_plus)
-
-instance
-  apply default
-  apply (rule permute_fset_zero)
-  apply (rule permute_fset_plus)
-  done
+instance proof
+  fix x :: "'a fset" and p q :: "perm"
+  show "0 \<bullet> x = x"
+    by (lifting permute_zero [where 'a="'a list"])
+  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"
+    by (lifting permute_plus [where 'a="'a list"])
+qed
 
 end
 

--- a/Pearl/Paper.thy	Thu Apr 08 09:12:13 2010 +0200
+++ b/Pearl/Paper.thy	Thu Apr 08 09:13:36 2010 +0200
@@ -338,7 +338,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,17 +363,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, 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.
+  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
@@ -892,10 +890,10 @@
 
   The following Isabelle/HOL command defines a concrete atom type called
   \emph{name}, which consists of atoms whose sort equals the string @{term
-  "''name''"}.
+  "''Thy.name''"}.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"}
   \end{isabelle}
 
   \noindent