--- a/LamEx.thy	Mon Nov 02 09:47:49 2009 +0100
+++ b/LamEx.thy	Mon Nov 02 11:15:26 2009 +0100
@@ -240,6 +240,75 @@
  *}
   apply (tactic {* tac @{context} 1 *}) *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {*
+  val rt = build_repabs_term @{context} t_r consts rty qty
+  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
+*}
+prove rg
+apply(atomize(full))
+ML_prf {*
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  (FIRST' [
+    rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
+    res_forall_rsp_tac ctxt,
+    res_exists_rsp_tac ctxt,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+    rtac refl,
+(*    rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
+    rtac reflex_thm,
+    atac,
+    (
+     (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
+    WEAK_LAMBDA_RES_TAC ctxt
+    ]);
+  fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms
+*}
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+prefer 2
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+apply (tactic {* r_mk_comb_tac_lam @{context} 1 *})
+
+
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}