--- a/src/HOL/Library/Quotient_Product.thy Fri Mar 23 14:18:43 2012 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Fri Mar 23 14:20:09 2012 +0100
@@ -13,8 +13,6 @@
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-declare [[map prod = prod_rel]]
-
lemma prod_rel_apply [simp]:
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
by (simp add: prod_rel_def)
@@ -45,6 +43,8 @@
apply (auto simp add: split_paired_all)
done
+declare [[map prod = (prod_rel, prod_quotient)]]
+
lemma Pair_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"