--- a/Quot/QuotProd.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotProd.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -92,6 +92,12 @@
 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
 
+lemma prod_rel_eq[id_simps]: "prod_rel op = op = \<equiv> op ="
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply auto
+  done
+
 section {* general setup for products *}
 
 declare [[map * = (prod_fun, prod_rel)]]