--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 23:34:30 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Thu Jul 29 10:16:33 2010 +0100
@@ -24,6 +24,7 @@
 thm alpha_bn_imps
 thm distinct
 thm eq_iff
+thm eq_iff_simps
 thm fv_defs
 thm perm_simps
 thm perm_laws
@@ -39,13 +40,13 @@
 term alpha_bn
 
 
-
 lemma a2:
   shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
   and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
   and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
+apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps 
+  alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
 done
 
 lemma [quot_respect]: 
@@ -59,24 +60,17 @@
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
 apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
+apply(simp only: eq_iff)
+apply(simp only: simp_thms)
 apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
-apply(assumption)
+apply(simp only: eq_iff)
+apply(tactic {* asm_full_simp_tac HOL_ss 1*})
 apply(simp only: fun_rel_def)
+apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2)
 apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2)
+apply(simp add: a2)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
 apply(simp only: fun_rel_def)
 apply(rule allI | rule impI)+