--- a/QuotMain.thy	Thu Nov 26 16:23:24 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
@@ -685,7 +685,6 @@
 
 section {* RepAbs injection tactic *}
 (*
-
 To prove that the regularised theorem implies the abs/rep injected, we first
 atomize it and then try:
 
@@ -835,6 +834,56 @@
     ])
 *}
 
+(*
+To prove that the regularised theorem implies the abs/rep injected, 
+we try:
+
+ 1) theorems 'trans2' from the appropriate QUOT_TYPE
+ 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 3) remove Ball/Bex from the right hand side
+ 4) use user-supplied RSP theorems
+ 5) remove rep_abs from the right side
+ 6) reflexivity of equality
+ 7) split applications of lifted type (apply_rsp)
+ 8) split applications of non-lifted type (cong_tac)
+ 9) apply extentionality
+10) reflexivity of the relation
+11) assumption
+    (Lambdas under respects may have left us some assumptions)
+12) proving obvious higher order equalities by simplifying fun_rel
+    (not sure if it is still needed?)
+13) unfolding lambda on one side
+14) simplifying (= ===> =) for simpler respectfulness
+
+*)
+
+ML {*
+fun r_mk_comb_tac' ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  REPEAT_ALL_NEW (FIRST' [
+    (K (print_tac "start")) THEN' (K no_tac), 
+    DT ctxt "1" (rtac trans_thm),
+    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+    DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    DT ctxt "4" (ball_rsp_tac ctxt),
+    DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+    DT ctxt "6" (bex_rsp_tac ctxt),
+    DT ctxt "7" (FIRST' (map rtac rsp_thms)),
+    DT ctxt "8" (rtac refl),
+    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+                  THEN' (RANGE [SOLVES' (quotient_tac quot_thm)]))),
+    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
+                (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)]))),
+    DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+    DT ctxt "C" (rtac @{thm ext}),
+    DT ctxt "D" (rtac reflex_thm),
+    DT ctxt "E" (atac),
+    DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
+    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
+    DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
+    ])
+*}
+
+
 
 (****************************************)
 (* cleaning of the theorem              *)