src/HOL/Library/Multiset.thy
changeset 67332 cb96edae56ef
parent 67051 e7e54a0b9197
child 67398 5eb932e604a2
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Jan 02 23:04:15 2018 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Jan 03 11:06:13 2018 +0100
     1.3 @@ -3869,7 +3869,7 @@
     1.4  
     1.5  subsection \<open>Size setup\<close>
     1.6  
     1.7 -lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
     1.8 +lemma size_multiset_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
     1.9    apply (rule ext)
    1.10    subgoal for x by (induct x) auto
    1.11    done
    1.12 @@ -3879,7 +3879,7 @@
    1.13      @{thm size_multiset_overloaded_def}
    1.14      @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
    1.15        size_union}
    1.16 -    @{thms multiset_size_o_map}
    1.17 +    @{thms size_multiset_o_map}
    1.18  \<close>
    1.19  
    1.20  subsection \<open>Lemmas about Size\<close>