| changeset 30242 | aea5d7fa7ef5 |
| parent 30235 | 58d147683393 |
| child 30660 | 53e1b1641f09 |
--- a/src/HOL/Import/HOL4Compat.thy Wed Mar 04 11:05:02 2009 +0100 +++ b/src/HOL/Import/HOL4Compat.thy Wed Mar 04 11:05:29 2009 +0100 @@ -73,7 +73,7 @@ lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)" by simp -lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)" +lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)" by simp consts