# HG changeset patch
# User haftmann
# Date 1163805626 -3600
# Node ID 13c33ad15303609afec1bd09889069e066041068
# Parent  f23e4e75dfd30953cdb85dabb11dfc8fa9395535
using class instance

diff -r f23e4e75dfd3 -r 13c33ad15303 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 18 00:20:24 2006 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 18 00:20:26 2006 +0100
@@ -49,13 +49,11 @@
   set_of :: "'a multiset => 'a set" where
   "set_of M = {x. x :# M}"
 
-instance multiset :: (type) "{plus, minus, zero}" ..
-
-defs (overloaded)
+instance multiset :: (type) "{plus, minus, zero, size}" 
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
   diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
   Zero_multiset_def [simp]: "0 == {#}"
-  size_def: "size M == setsum (count M) (set_of M)"
+  size_def: "size M == setsum (count M) (set_of M)" ..
 
 definition
   multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where