diff -r e08e3c29dbc0 -r 2205b572bc9b Nominal/Ex/CoreHaskell.thy
--- a/Nominal/Ex/CoreHaskell.thy	Tue May 11 14:58:46 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Tue May 11 17:16:57 2010 +0200
@@ -203,9 +203,9 @@
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bv2[symmetric])
-  apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
   apply (simp add: fv_supp)
+  apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric])
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
   apply (rule finite_Diff)
@@ -395,18 +395,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a08)
@@ -435,18 +433,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
                 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a15)
@@ -476,18 +472,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a29)
@@ -516,18 +510,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a30)
@@ -557,18 +549,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a32)
@@ -598,18 +588,16 @@
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
                 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst)
     apply (simp add: eqvts)
-    apply (simp add: eqvts[symmetric])
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric])
     apply (rule conjI)
     apply (rule supp_perm_eq)
     apply (simp add: eqvts)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply (simp add: eqvts)
     apply (subst supp_perm_eq)
     apply (subst supp_finite_atom_set)
-    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
-    apply (simp add: eqvts)
+    apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt)
     apply assumption
     apply (simp add: fresh_star_minus_perm)
     apply (rule a34)
@@ -659,13 +647,12 @@
 (* for the moment, we force it to be       *)
 
 (*declare permute_pure[eqvt]*)
-(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *)
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *)
 
 thm eqvts
 thm eqvts_raw
 
 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt]
-declare alpha_gen_eqvt[eqvt]
 
 equivariance alpha_tkind_raw