--- a/src/HOL/Lifting_Option.thy Tue Feb 18 23:03:47 2014 +0100
+++ b/src/HOL/Lifting_Option.thy Tue Feb 18 23:03:49 2014 +0100
@@ -39,10 +39,6 @@
using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
by (auto iff: fun_eq_iff split: option.split)
-lemma reflp_rel_option[reflexivity_rule]:
- "reflp R \<Longrightarrow> reflp (rel_option R)"
- unfolding reflp_def split_option_all by simp
-
lemma left_total_rel_option[reflexivity_rule]:
"left_total R \<Longrightarrow> left_total (rel_option R)"
unfolding left_total_def split_option_all split_option_ex by simp