src/HOL/Lifting_Option.thy
changeset 55945 e96383acecf9
parent 55564 e81ee43ab290
child 56092 1ba075db8fe4
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Mar 06 15:29:18 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Mar 06 15:40:33 2014 +0100
     1.3 @@ -86,11 +86,11 @@
     1.4    by (rule option.rel_inject)
     1.5  
     1.6  lemma Some_transfer [transfer_rule]: "(A ===> rel_option A) Some Some"
     1.7 -  unfolding fun_rel_def by simp
     1.8 +  unfolding rel_fun_def by simp
     1.9  
    1.10  lemma case_option_transfer [transfer_rule]:
    1.11    "(B ===> (A ===> B) ===> rel_option A ===> B) case_option case_option"
    1.12 -  unfolding fun_rel_def split_option_all by simp
    1.13 +  unfolding rel_fun_def split_option_all by simp
    1.14  
    1.15  lemma map_option_transfer [transfer_rule]:
    1.16    "((A ===> B) ===> rel_option A ===> rel_option B) map_option map_option"
    1.17 @@ -99,7 +99,7 @@
    1.18  lemma option_bind_transfer [transfer_rule]:
    1.19    "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
    1.20      Option.bind Option.bind"
    1.21 -  unfolding fun_rel_def split_option_all by simp
    1.22 +  unfolding rel_fun_def split_option_all by simp
    1.23  
    1.24  end
    1.25