diff -r 8f51702e1f2e -r 52730e5ec8cb Nominal/GPerm.thy
--- a/Nominal/GPerm.thy	Wed May 23 23:57:27 2012 +0100
+++ b/Nominal/GPerm.thy	Thu May 24 10:17:32 2012 +0200
@@ -36,12 +36,12 @@
   by (metis valid_perm_def image_set length_map len_set_eq_distinct)
 
 definition
-  perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool" (infix "\<approx>" 50)
+  perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool"
 where
-  "x \<approx> y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)"
+  "perm_eq x y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)"
 
 lemma perm_eq_sym[sym]:
-  "x \<approx> y \<Longrightarrow> y \<approx> x"
+  "perm_eq x y \<Longrightarrow> perm_eq y x"
   by (auto simp add: perm_eq_def)
 
 lemma perm_eq_equivp:
@@ -159,7 +159,7 @@
   by (metis uminus_perm_raw_def)
 
 lemma uminus_perm_raw_rsp[simp]:
-  "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"
+  "perm_eq x y \<Longrightarrow> perm_eq (map swap_pair x) (map swap_pair y)"
   by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
 lemma fst_snd_map_pair[simp]:
@@ -233,11 +233,11 @@
   done
 
 lemma perm_add_raw_rsp[simp]:
-  "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"
+  "perm_eq x y \<Longrightarrow> perm_eq xa ya \<Longrightarrow> perm_eq (perm_add_raw x xa) (perm_add_raw y ya)"
   by (simp add: fun_eq_iff perm_add_apply perm_eq_def)
 
 lemma [simp]:
-  "a \<approx> a \<longleftrightarrow> valid_perm a"
+  "perm_eq a a \<longleftrightarrow> valid_perm a"
   by (simp_all add: perm_eq_def)
 
 instantiation gperm :: (type) group_add
@@ -276,7 +276,7 @@
   by (induct y) (auto split: if_splits)
 
 lemma perm_eq_not_eq_same:
-  "x \<approx> y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}"
+  "perm_eq x y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}"
   unfolding perm_eq_def set_eq_iff
   apply auto
   apply (subgoal_tac "perm_apply x a = b")
@@ -315,7 +315,7 @@
   by (metis in_set_in_dpr2 pair_perm_apply perm_apply_in_set valid_perm_def)
 
 lemma dest_perm_raw_eq[simp]:
-  "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = (x \<approx> y)"
+  "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = perm_eq x y"
   apply (auto simp add: perm_eq_def)
   apply (metis in_set_in_dpr3 fun_eq_iff)
   unfolding dest_perm_raw_def
@@ -371,8 +371,8 @@
   by simp (rule sorted_sort_id[OF sorted_sort])
 
 lemma valid_dest_perm_raw_eq[simp]:
-  "valid_perm p \<Longrightarrow> dest_perm_raw p \<approx> p"
-  "valid_perm p \<Longrightarrow> p \<approx> dest_perm_raw p"
+  "valid_perm p \<Longrightarrow> perm_eq (dest_perm_raw p) p"
+  "valid_perm p \<Longrightarrow> perm_eq p (dest_perm_raw p)"
   by (simp_all add: dest_perm_raw_eq[symmetric])
 
 lemma mk_perm_dest_perm[code abstype]: