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