--- a/LamEx.thy	Fri Dec 04 08:19:56 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 09:10:31 2009 +0100
@@ -312,40 +312,32 @@
   "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s"
 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *})
 prefer 2
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
-apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 apply (simp only: perm_prs)
 prefer 2
-apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 prefer 3
-apply (tactic {* clean_tac @{context} [quot] 1 *})
-
-thm all_prs
-thm REP_ABS_RSP
-thm ball_reg_eqv_range
-
-
-thm perm_lam_def
+apply (tactic {* clean_tac @{context} 1 *})
 apply (simp only: perm_prs)
-
-apply (tactic {* regularize_tac @{context} [quot] 1 *})
+(*apply (tactic {* regularize_tac @{context} 1 *})*)
 
 done