diff -r 455a9f89c47d -r 7aa35601ff65 src/HOL/Library/Quotient_Product.thy
--- a/src/HOL/Library/Quotient_Product.thy Thu May 24 13:56:21 2012 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Thu May 24 14:20:23 2012 +0200
@@ -27,12 +27,18 @@
shows "prod_rel (op =) (op =) = (op =)"
by (simp add: fun_eq_iff)
-lemma prod_reflp [reflp_preserve]:
+lemma prod_reflp [reflexivity_rule]:
assumes "reflp R1"
assumes "reflp R2"
shows "reflp (prod_rel R1 R2)"
using assms by (auto intro!: reflpI elim: reflpE)
+lemma prod_left_total [reflexivity_rule]:
+ assumes "left_total R1"
+ assumes "left_total R2"
+ shows "left_total (prod_rel R1 R2)"
+using assms by (auto intro!: left_totalI elim!: left_totalE)
+
lemma prod_equivp [quot_equiv]:
assumes "equivp R1"
assumes "equivp R2"