--- a/src/HOL/Library/Multiset.thy Tue Jan 02 23:04:15 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Jan 03 11:06:13 2018 +0100
@@ -3869,7 +3869,7 @@
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
@@ -3879,7 +3879,7 @@
@{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>