--- a/Nominal/Ex/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -94,6 +94,7 @@
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
+using [[simproc del: alpha_lst]]
 apply(simp_all)
 apply(erule_tac c="()" in Abs_lst1_fcb2')
 apply(simp_all add: pure_fresh fresh_star_def)[3]
@@ -124,6 +125,7 @@
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 apply(auto simp add: fresh_star_def)[3]
+using [[simproc del: alpha_lst]]
 apply(simp_all)
 apply(erule conjE)+
 apply(erule_tac Abs_lst1_fcb2)
@@ -169,6 +171,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule conjE)+
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
@@ -202,6 +205,7 @@
 apply(simp)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply(auto)
 apply (erule_tac c="()" in Abs_lst1_fcb2)
 apply(simp add: supp_removeAll fresh_def)
@@ -229,6 +233,7 @@
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp add: fresh_minus_atom_set)
@@ -254,6 +259,7 @@
   apply(simp add: eqvt_def height_graph_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply (erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
@@ -276,9 +282,11 @@
   unfolding eqvt_def subst_graph_def
   apply(simp)
   apply(rule TrueI)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+
+  using [[simproc del: alpha_lst]]
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
@@ -306,8 +314,10 @@
 text {* same lemma but with subst.induction *}
 lemma forget2:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-  by (induct t x s rule: subst.induct)
-     (auto simp add:  fresh_at_base fresh_Pair)
+  apply(induct t x s rule: subst.induct)
+  using [[simproc del: alpha_lst]]
+  apply(auto simp add:  flip_fresh_fresh fresh_Pair fresh_at_base)
+  done
 
 lemma fresh_fact:
   fixes z::"name"
@@ -467,6 +477,7 @@
   apply(auto)[1]
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule conjE)+
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
@@ -498,6 +509,7 @@
   apply(auto)[3]
   apply(all_trivials)
   apply(simp)
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule_tac c="()" in Abs_lst1_fcb2')
   apply(simp add: pure_fresh)
@@ -526,6 +538,7 @@
   apply(all_trivials)
   apply(simp)
   apply(simp)
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule conjE)
   apply(erule Abs_lst1_fcb2')
@@ -582,6 +595,7 @@
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(elim conjE)
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
@@ -641,6 +655,7 @@
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply simp_all[3]
   apply blast
   apply (case_tac b)
@@ -649,6 +664,7 @@
   apply blast
   apply blast
   apply (simp add: Abs1_eq_iff fresh_star_def)
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply (simp add: Abs_fresh_iff)
@@ -692,6 +708,7 @@
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply simp_all
 apply blast
 apply blast
@@ -718,6 +735,7 @@
   apply (simp add: eqvt_def map_term_graph_def)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (erule Abs_lst1_fcb)
   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
@@ -890,13 +908,16 @@
   apply(rule_tac y="b" in lam.exhaust)
   apply(auto)[3]
   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply(auto)[3]
   apply(drule_tac x="name" in meta_spec)
   apply(drule_tac x="name" in meta_spec)
   apply(drule_tac x="lam" in meta_spec)
   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
+  using [[simproc del: alpha_lst]]
   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
+  using [[simproc del: alpha_lst]]
   apply simp_all
   apply (simp add: abs_same_binder)
   apply (erule_tac c="()" in Abs_lst1_fcb2)