--- a/IntEx.thy	Sat Nov 28 03:07:38 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 04:37:04 2009 +0100
@@ -161,7 +161,7 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***)
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
@@ -236,49 +236,3 @@
 done
 
 
-(*
-
-ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
-  (REPEAT1 o FIRST1) 
-    [(K (print_tac "start")) THEN' (K no_tac), 
-     DT ctxt "1" (rtac trans_thm),
-     DT ctxt "2" (LAMBDA_RES_TAC ctxt),
-     DT ctxt "3" (ball_rsp_tac ctxt),
-     DT ctxt "4" (bex_rsp_tac ctxt),
-     DT ctxt "5" (FIRST' (map rtac rsp_thms)),
-     DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
-     DT ctxt "7" (rtac refl),
-     DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
-     DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
-     DT ctxt "A" (rtac @{thm ext}),
-     DT ctxt "B" (rtac reflex_thm),
-     DT ctxt "C" (atac),
-     DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
-     DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
-     DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
-*}
-
-ML {* 
-inj_repabs_trm @{context} (reg_atrm, aqtrm) 
-  |> Syntax.check_term @{context}
-*}
-
-
-ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
-ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
-
-prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
-apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
-done
-
-ML {*
-inj_repabs_trm @{context} (reg_atrm, aqtrm)  
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-*)
-
-