--- a/Quot/QuotProd.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotProd.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -82,14 +82,23 @@
   apply(simp add: Quotient_abs_rep[OF q2])
   done
 
+lemma split_rsp[quot_respect]:
+  shows "((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 \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
+  shows "prod_fun id id = id"
+  by (simp add: prod_fun_def)
 
 lemma prod_rel_eq[id_simps]: 
-  shows "prod_rel (op =) (op =) \<equiv> (op =)"
-  apply (rule eq_reflection)
-  apply (simp add: expand_fun_eq)
-  done
+  shows "prod_rel (op =) (op =) = (op =)"
+  by (simp add: expand_fun_eq)
+ 
 
 end