--- 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
 

--- a/QuotMain.thy	Fri Dec 04 08:19:56 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:10:31 2009 +0100
@@ -735,10 +735,8 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [resolve_tac (quotient_rules_get ctxt),
-     (* For functional identity quotients, (op = ---> op =) *)
-     (* TODO: think about the other way around, if we need to shorten the relation *)
-     CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
+    [rtac @{thm IDENTITY_QUOTIENT},
+     resolve_tac (quotient_rules_get ctxt)])
 *}
 
 
@@ -954,11 +952,12 @@
     NDT ctxt "D" (resolve_tac rel_refl),
 
     (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac),
+    NDT ctxt "E" (atac)
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))])
+    (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))*)
+    ])
 *}
 
 ML {*