--- 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