--- a/QuotMain.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 11:53:20 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),
@@ -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.