Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
overloaded 0
authorpaulson
Wed, 24 May 2000 18:43:39 +0200
changeset 8953 40ae3d4122bd
parent 8952 921c35be6ffb
child 8954 4fbdda40bb5f
overloaded 0
src/HOL/Induct/Multiset.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle