--- a/QuotMain.thy	Mon Nov 30 12:26:08 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 13:58:05 2009 +0100
@@ -136,6 +136,7 @@
 
 end
 
+(* EQUALS_RSP is stronger *)
 lemma equiv_trans2:
   assumes e: "EQUIV R"
   and     ac: "R a c"
@@ -927,13 +928,13 @@
     NDT ctxt "2" (lambda_res_tac ctxt),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    NDT ctxt "3" (rtac @{thm ball_rsp}),
 
     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
     NDT ctxt "4" (ball_rsp_tac ctxt),
 
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+    NDT ctxt "5" (rtac @{thm bex_rsp}),
 
     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
     NDT ctxt "6" (bex_rsp_tac ctxt),
@@ -946,7 +947,7 @@
 
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
@@ -1030,8 +1031,7 @@
 
 ML {*
 fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot)
+  (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
 *}
 
 (* Rewrites the term with LAMBDA_PRS thm.
@@ -1102,6 +1102,25 @@
           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
 *}
 
+(*
+ Cleaning the theorem consists of 5 kinds of rewrites.
+ These rewrites can be done independently and in any order.
+
+ - LAMBDA_PRS:
+     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x)))       \<equiv>   ?f
+ - Rewriting with definitions from the argument defs
+     (Abs) OldConst (Rep Args)                       \<equiv>   NewConst Args
+ - QUOTIENT_REL_REP:
+     Rel (Rep x) (Rep y)                             \<equiv>   x = y
+ - FORALL_PRS (and the same for exists: EXISTS_PRS)
+     \<forall>x\<in>Respects R. (abs ---> id) ?f                 \<equiv>   \<forall>x. ?f
+ - applic_prs
+     Abs1 ((Abs2 --> Rep1) f (Rep2 args))            \<equiv>   f args
+
+ The first one is implemented as a conversion (fast).
+ The second and third one are a simp_tac (fast).
+ The last two are EqSubst (slow).
+*)
 ML {*
 fun clean_tac lthy quot defs aps =
   let