src/HOL/Library/Multiset.thy
changeset 62082 614ef6d7a6b6
parent 61955 e96292f32c3c
child 62208 ad43b3ab06e4
--- a/src/HOL/Library/Multiset.thy	Wed Jan 06 13:04:31 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Jan 06 13:04:31 2016 +0100
@@ -2506,6 +2506,7 @@
 
 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}