# HG changeset patch
# User paulson
# Date 959186619 -7200
# Node ID 40ae3d4122bda820a178d32a96f0d9def48124f5
# Parent  921c35be6ffb89bf0623f3219690c4fa9f9e1b0f
overloaded 0

diff -r 921c35be6ffb -r 40ae3d4122bd src/HOL/Induct/Multiset.thy
--- a/src/HOL/Induct/Multiset.thy	Wed May 24 18:43:16 2000 +0200
+++ b/src/HOL/Induct/Multiset.thy	Wed May 24 18:43:39 2000 +0200
@@ -33,9 +33,10 @@
   empty_def  "{#}   == Abs_multiset(%a. 0)"
   single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)"
   union_def  "M+N   == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)"
-  diff_def  "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
+  diff_def   "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
   set_of_def "set_of M == {x. M :# x}"
-  size_def "size (M) == setsum (count M) (set_of M)"
+  size_def   "size (M) == setsum (count M) (set_of M)"
+  Zero_def   "0 == {#}"
 
 constdefs
   mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set"