src/HOL/Option.thy
changeset 40968 a6fcd305f7dc
parent 40609 efb0d7878538
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Option.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/Option.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
     1.5    by (rule ext) (simp split: sum.split)
     1.6  
     1.7 -type_mapper Option.map proof -
     1.8 +type_lifting Option.map proof -
     1.9    fix f g x
    1.10    show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
    1.11      by (cases x) simp_all