src/HOL/Lifting_Option.thy
changeset 55564 e81ee43ab290
parent 55525 70b7e91fa1f9
child 55945 e96383acecf9
     1.1 --- a/src/HOL/Lifting_Option.thy	Tue Feb 18 23:03:47 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Tue Feb 18 23:03:49 2014 +0100
     1.3 @@ -39,10 +39,6 @@
     1.4  using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
     1.5  by (auto iff: fun_eq_iff split: option.split)
     1.6  
     1.7 -lemma reflp_rel_option[reflexivity_rule]:
     1.8 -  "reflp R \<Longrightarrow> reflp (rel_option R)"
     1.9 -  unfolding reflp_def split_option_all by simp
    1.10 -
    1.11  lemma left_total_rel_option[reflexivity_rule]:
    1.12    "left_total R \<Longrightarrow> left_total (rel_option R)"
    1.13    unfolding left_total_def split_option_all split_option_ex by simp