src/HOL/Lifting_Sum.thy
changeset 55564 e81ee43ab290
parent 55414 eab03e9cee8a
child 55931 62156e694f3d
--- a/src/HOL/Lifting_Sum.thy	Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Sum.thy	Tue Feb 18 23:03:49 2014 +0100
@@ -26,10 +26,6 @@
 using assms
 by (auto simp add: Domainp_iff split_sum_ex iff: fun_eq_iff split: sum.split)
 
-lemma reflp_sum_rel[reflexivity_rule]:
-  "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (sum_rel R1 R2)"
-  unfolding reflp_def split_sum_all sum_rel_simps by fast
-
 lemma left_total_sum_rel[reflexivity_rule]:
   "left_total R1 \<Longrightarrow> left_total R2 \<Longrightarrow> left_total (sum_rel R1 R2)"
   using assms unfolding left_total_def split_sum_all split_sum_ex by simp