--- a/FSet.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/FSet.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -328,7 +328,7 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
@@ -350,52 +350,52 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(rule cheat)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 
@@ -444,8 +444,8 @@
   apply (assumption)
   done
 
-ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun r_mk_comb_tac_fset' lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -460,65 +460,65 @@
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule IDENTITY_QUOTIENT)
 apply (rule FUN_QUOTIENT)
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *})
 done
 

--- 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 *})

--- a/LFex.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/LFex.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -269,197 +269,197 @@
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
   val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
 *}
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* r_mk_comb_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
 done
 
 print_quotients

--- a/LamEx.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/LamEx.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -264,12 +264,6 @@
 (* Construction Site code *)
 
 
-
-
-
-
-
-
 fun
   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
 where

--- a/QuotMain.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -878,7 +878,7 @@
 *}
 
 ML {*
-fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            lambda_res_tac ctxt,
            rtac @{thm RES_FORALL_RSP},
@@ -899,8 +899,8 @@
            weak_lambda_res_tac ctxt,
            CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
 
-fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 (*
@@ -927,7 +927,7 @@
 *)
 
 ML {*
-fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
   
@@ -990,8 +990,8 @@
 *}
 
 ML {*
-fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 
@@ -1245,7 +1245,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+               all_inj_repabs_tac lthy rty quot rel_refl trans2 rsp_thms,
                clean_tac lthy quot defs aps]]
     end) lthy
 *}