src/HOL/Lifting_Option.thy
changeset 56518 beb3b6851665
parent 56092 1ba075db8fe4
child 56519 c1048f5bbb45
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:13 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:14 2014 +0200
     1.3 @@ -39,11 +39,11 @@
     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 left_total_rel_option[reflexivity_rule]:
     1.8 +lemma left_total_rel_option[transfer_rule]:
     1.9    "left_total R \<Longrightarrow> left_total (rel_option R)"
    1.10    unfolding left_total_def split_option_all split_option_ex by simp
    1.11  
    1.12 -lemma left_unique_rel_option [reflexivity_rule]:
    1.13 +lemma left_unique_rel_option [transfer_rule]:
    1.14    "left_unique R \<Longrightarrow> left_unique (rel_option R)"
    1.15    unfolding left_unique_def split_option_all by simp
    1.16