src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Thu Mar 01 21:35:49 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Mar 02 09:35:32 2012 +0100
@@ -476,6 +476,8 @@
 lemma finite_set_of [iff]: "finite (set_of M)"
   using count [of M] by (simp add: multiset_def set_of_def)
 
+lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
+  unfolding set_of_def[symmetric] by simp
 
 subsubsection {* Size *}