src/HOL/Library/Multiset.thy
changeset 45694 4a8743618257
parent 45608 13b101cee425
child 45866 e62b319c7696
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -10,10 +10,13 @@
     1.4  
     1.5  subsection {* The type of multisets *}
     1.6  
     1.7 -typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
     1.8 +definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
     1.9 +
    1.10 +typedef (open) 'a multiset = "multiset :: ('a => nat) set"
    1.11    morphisms count Abs_multiset
    1.12 +  unfolding multiset_def
    1.13  proof
    1.14 -  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
    1.15 +  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
    1.16  qed
    1.17  
    1.18  lemmas multiset_typedef = Abs_multiset_inverse count_inverse count