--- a/src/HOL/Lifting_Product.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Product.thy Tue Feb 18 23:03:49 2014 +0100
@@ -30,12 +30,6 @@
shows "Domainp (prod_rel T1 T2) = (prod_pred P1 P2)"
using assms unfolding prod_rel_def prod_pred_def by blast
-lemma reflp_prod_rel [reflexivity_rule]:
- assumes "reflp R1"
- assumes "reflp R2"
- shows "reflp (prod_rel R1 R2)"
-using assms by (auto intro!: reflpI elim: reflpE)
-
lemma left_total_prod_rel [reflexivity_rule]:
assumes "left_total R1"
assumes "left_total R2"