--- a/Nominal/Ex/SingleLet.thy	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 11 19:53:57 2010 +0800
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = {atom x}"
 
+
+
 thm alpha_sym_thms
 thm alpha_trans_thms
 thm size_eqvt
@@ -34,9 +36,10 @@
 thm perm_simps
 thm perm_laws
 thm funs_rsp
+thm constrs_rsp
 
-declare size_rsp[quot_respect]
-declare funs_rsp[quot_respect]
+declare constrs_rsp[quot_respect]
+(* declare funs_rsp[quot_respect] *)
 
 typ trm
 typ assg
@@ -47,33 +50,6 @@
 term fv_trm
 term alpha_bn
 
-lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
-
-ML {* 
-  val pre_ss = @{thms fun_rel_def}
-  val post_ss = @{thms alphas prod_alpha_def prod_rel.simps 
-    prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps}
-
-  val tac = 
-    asm_full_simp_tac (HOL_ss addsimps pre_ss)
-    THEN' REPEAT o (resolve_tac @{thms allI impI})
-    THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} 
-    THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss))
-*}
-
-lemma [quot_respect]: 
-  "(op= ===> alpha_trm_raw) Var_raw Var_raw"
-  "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw"
-  "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw"
-  "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw"
-  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw)
-     Foo_raw Foo_raw"
-  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
-  "(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(tactic {* ALLGOALS tac *})
-sorry
-
 lemma [quot_respect]:
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
 apply(simp)