equal
deleted
inserted
replaced
71 by simp; |
71 by simp; |
72 |
72 |
73 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)" |
73 lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)" |
74 by simp |
74 by simp |
75 |
75 |
76 lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)" |
76 lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)" |
77 by simp |
77 by simp |
78 |
78 |
79 consts |
79 consts |
80 IS_SOME :: "'a option => bool" |
80 IS_SOME :: "'a option => bool" |
81 IS_NONE :: "'a option => bool" |
81 IS_NONE :: "'a option => bool" |