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