src/HOL/Library/Multiset.thy

   rel_mset'.induct[unfolded rel_mset_rel_mset'[symmetric]]
 
 
 subsection \<open>Size setup\<close>
 
-lemma multiset_size_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
+lemma size_multiset_o_map: "size_multiset g \<circ> image_mset f = size_multiset (g \<circ> f)"
   apply (rule ext)
   subgoal for x by (induct x) auto
   done
 
 setup \<open>
   BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
     @{thm size_multiset_overloaded_def}
     @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
       size_union}
-    @{thms multiset_size_o_map}
+    @{thms size_multiset_o_map}
 \<close>
 
 subsection \<open>Lemmas about Size\<close>
 
 lemma size_mset_SucE: "size A = Suc n \<Longrightarrow> (\<And>a B. A = {#a#} + B \<Longrightarrow> size B = n \<Longrightarrow> P) \<Longrightarrow> P"