equal
deleted
inserted
replaced
474 by (auto simp add: set_of_def) |
474 by (auto simp add: set_of_def) |
475 |
475 |
476 lemma finite_set_of [iff]: "finite (set_of M)" |
476 lemma finite_set_of [iff]: "finite (set_of M)" |
477 using count [of M] by (simp add: multiset_def set_of_def) |
477 using count [of M] by (simp add: multiset_def set_of_def) |
478 |
478 |
|
479 lemma finite_Collect_mem [iff]: "finite {x. x :# M}" |
|
480 unfolding set_of_def[symmetric] by simp |
479 |
481 |
480 subsubsection {* Size *} |
482 subsubsection {* Size *} |
481 |
483 |
482 instantiation multiset :: (type) size |
484 instantiation multiset :: (type) size |
483 begin |
485 begin |