diff -r 68c1f378a70a -r 0879d144aaa3 Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Tue Jan 26 09:28:32 2010 +0100
+++ b/Quot/QuotProd.thy	Tue Jan 26 09:54:43 2010 +0100
@@ -74,6 +74,16 @@
   apply (simp add: Quotient_abs_rep[OF q2])
   done
 
+lemma split_rsp[quot_respect]:
+  "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
+  by auto
+
+lemma split_prs[quot_preserve]:
+  assumes q1: "Quotient R1 Abs1 Rep1"
+  and     q2: "Quotient R2 Abs2 Rep2"
+  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+
 lemma prod_fun_id[id_simps]:
   shows "prod_fun id id = id"
   by (simp add: prod_fun_def)