src/HOL/Sum_Type.thy
changeset 40968 a6fcd305f7dc
parent 40610 70776ecfe324
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Sum_Type.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
     1.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
     1.6  
     1.7 -type_mapper sum_map proof -
     1.8 +type_lifting sum_map proof -
     1.9    fix f g h i s
    1.10    show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
    1.11      by (cases s) simp_all