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}