diff -r 9c33c0809733 -r 1c245f6911dd IntEx.thy
--- a/IntEx.thy	Sat Nov 28 05:29:30 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 05:43:18 2009 +0100
@@ -147,8 +147,6 @@
 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
-lemma cheat: "P" sorry
-
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
@@ -178,7 +176,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 {* all_r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 done
 
 lemma plus_assoc_pre:
@@ -236,49 +234,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
-*}
-
-*)
-
-