--- a/FIXME-TODO	Fri Dec 04 09:25:27 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 09:33:32 2009 +0100
@@ -38,4 +38,8 @@
 - use lower-case letters where appropriate in order
   to make Markus happy
 
-- add tests for adding theorems to the various thm lists
\ No newline at end of file
+- add tests for adding theorems to the various thm lists
+
+
+
+- Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc.

--- a/LamEx.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -340,5 +340,3 @@
 (*apply (tactic {* regularize_tac @{context} 1 *})*)
 sorry
 
-done
-

--- a/QuotList.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -16,6 +16,7 @@
 
 lemma LIST_REL_EQ:
   shows "LIST_REL (op =) \<equiv> (op =)"
+apply(rule eq_reflection)
 unfolding expand_fun_eq
 apply(rule allI)+
 apply(induct_tac x xa rule: list_induct2')

--- a/QuotMain.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -967,7 +967,7 @@
 (* A faster version *)
 
 ML {*
-fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
   ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
@@ -992,29 +992,30 @@
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 | _ $ _ $ _ =>
-    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)]
+    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)]
 ) i)
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac' ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_fast ctxt quot_thms trans2,
+    inj_repabs_tac_fast ctxt trans2,
     NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
     NDT ctxt "E" (atac),
     NDT ctxt "D" (resolve_tac rel_refl),
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt))
+(*    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
+    ])
 *}
 
 ML {*
-fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)
+fun all_inj_repabs_tac' ctxt rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2)
 *}
 
 

--- a/QuotScript.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -137,7 +137,7 @@
 
 lemma FUN_REL_EQ:
   "(op =) ===> (op =) \<equiv> (op =)"
-by (simp add: expand_fun_eq)
+by (rule eq_reflection) (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT:
   assumes q1: "QUOTIENT R1 abs1 rep1"