changeset 41505 | 6d19301074cf |
parent 41372 | 551eb49a6e91 |
child 42809 | 5b45125b15ba |
--- a/src/HOL/Library/Multiset.thy Mon Jan 10 22:03:24 2011 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Jan 11 14:12:37 2011 +0100 @@ -1643,7 +1643,7 @@ @{term "{#x+x|x:#M. x<c#}"}. *} -type_lifting image_mset: image_mset proof - +enriched_type image_mset: image_mset proof - fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)" proof