src/HOL/Option.thy
changeset 63648 f9f3006a5579
parent 63343 fb5d8a50c641
child 66364 fa3247e6ee4b
     1.1 --- a/src/HOL/Option.thy	Tue Aug 09 23:29:54 2016 +0200
     1.2 +++ b/src/HOL/Option.thy	Wed Aug 10 09:33:54 2016 +0200
     1.3 @@ -100,13 +100,13 @@
     1.4    by (auto split: option.split)
     1.5  
     1.6  lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
     1.7 -  by (simp add: map_option_case split add: option.split)
     1.8 +  by (simp add: map_option_case split: option.split)
     1.9  
    1.10  lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
    1.11  by(cases x) simp_all
    1.12  
    1.13  lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
    1.14 -  by (simp add: map_option_case split add: option.split)
    1.15 +  by (simp add: map_option_case split: option.split)
    1.16  
    1.17  lemma map_option_o_case_sum [simp]:
    1.18      "map_option f o case_sum g h = case_sum (map_option f o g) (map_option f o h)"