src/HOL/Library/Multiset.thy
changeset 40968 a6fcd305f7dc
parent 40950 a370b0fb6f09
child 41069 6fabc0414055
     1.1 --- a/src/HOL/Library/Multiset.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -1631,7 +1631,7 @@
     1.4    @{term "{#x+x|x:#M. x<c#}"}.
     1.5  *}
     1.6  
     1.7 -type_mapper image_mset proof -
     1.8 +type_lifting image_mset proof -
     1.9    fix f g A show "image_mset f (image_mset g A) = image_mset (\<lambda>x. f (g x)) A"
    1.10      by (induct A) simp_all
    1.11  next