src/HOL/Library/Multiset.thy
changeset 49834 b27bbb021df1
parent 49823 1c146fa7701e
child 51126 df86080de4cb
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
     1.6  
     1.7 -typedef (open) 'a multiset = "multiset :: ('a => nat) set"
     1.8 +typedef 'a multiset = "multiset :: ('a => nat) set"
     1.9    morphisms count Abs_multiset
    1.10    unfolding multiset_def
    1.11  proof