src/HOL/Import/HOL4Compat.thy
changeset 30235 58d147683393
parent 29044 45dfd04a972e
child 30660 53e1b1641f09
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
     1.5    by simp
     1.6  
     1.7 -lemma OPTION_MAP_DEF: "(!f x. option_map f (Some x) = Some (f x)) & (!f. option_map f None = None)"
     1.8 +lemma OPTION_MAP_DEF: "(!f x. Option.map f (Some x) = Some (f x)) & (!f. Option.map f None = None)"
     1.9    by simp
    1.10  
    1.11  consts