# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259922889 -3600
# Node ID fdfeef0399f748a0c3d741bd00670f2777486f90
# Parent  cc1f240d8cf468578407af877abac9e3c59701aa# Parent  ebfd747b47ab07605d1881ae19348e4bd1222e0d
merged

diff -r cc1f240d8cf4 -r fdfeef0399f7 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 11:34:21 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:34:49 2009 +0100
@@ -136,16 +136,6 @@
 
 end
 
-(* EQUALS_RSP is stronger *)
-lemma equiv_trans2:
-  assumes e: "EQUIV R"
-  and     ac: "R a c"
-  and     bd: "R b d"
-  shows "R a b = R c d"
-using ac bd e
-unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def
-by (blast)
-
 section {* type definition for the quotient type *}
 
 (* the auxiliary data for the quotient types *)
@@ -1343,7 +1333,8 @@
       val rthm' = atomize_thm rthm
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
-      val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
+      val quotients = quotient_rules_get lthy
+      val trans2 = map (fn x => @{thm EQUALS_RSP} OF [x]) quotients
       val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i}
     in
       EVERY1
diff -r cc1f240d8cf4 -r fdfeef0399f7 QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 11:34:21 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 11:34:49 2009 +0100
@@ -268,8 +268,8 @@
 
 lemma EQUALS_RSP:
   assumes q: "QUOTIENT R Abs Rep"
-  and     a: "R x1 x2" "R y1 y2"
-  shows "R x1 y1 = R x2 y2"
+  and     a: "R xa xb" "R ya yb"
+  shows "R xa ya = R xb yb"
 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
 using a by blast