src/HOL/Library/Multiset.thy
changeset 46756 faf62905cd53
parent 46730 e3b99d0231bc
child 46921 aa862ff8a8a9
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 01 21:35:49 2012 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Mar 02 09:35:32 2012 +0100
     1.3 @@ -476,6 +476,8 @@
     1.4  lemma finite_set_of [iff]: "finite (set_of M)"
     1.5    using count [of M] by (simp add: multiset_def set_of_def)
     1.6  
     1.7 +lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
     1.8 +  unfolding set_of_def[symmetric] by simp
     1.9  
    1.10  subsubsection {* Size *}
    1.11