diff -r 75af61f32ece -r f1c0a66284d3 IntEx.thy
--- a/IntEx.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -143,8 +143,8 @@
 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
 
 
-ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
 lemma "PLUS a b = PLUS b a"
@@ -154,29 +154,29 @@
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
 apply(tactic {* clean_tac @{context} [quot] defs aps 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*})
-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*})
-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*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 done
 
 lemma plus_assoc_pre:
@@ -190,7 +190,7 @@
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
@@ -207,8 +207,13 @@
 sorry
 
 lemma "foldl PLUS x [] = x"
-apply (tactic {* lift_tac_intex @{context} @{thm ho_tst} 1 *})
-apply (simp_all only: map_prs foldl_prs)
+apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
+apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(rule foldl_prs) 
+apply(simp add: map_prs)
+ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
+ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
 sorry
 
 (*
@@ -216,18 +221,10 @@
   does not work.
 *)
 
-ML {*
-  regularize_trm @{context} 
-    @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
-    @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})