# HG changeset patch
# User kleing
# Date 1111791656 -3600
# Node ID cc3776f004e298e8d04f78e7cc531a6eb2051e65
# Parent  4066f01f1bebe49c46e76ac51d936d4ab55f227c
fixed typo (multiset_append)
moved multiset_of_complement_union from ex/Sorting

diff -r 4066f01f1beb -r cc3776f004e2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Mar 25 17:47:11 2005 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Mar 26 00:00:56 2005 +0100
@@ -742,7 +742,7 @@
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
  by (induct_tac x, auto) 
 
-lemma multset_of_append[simp]: 
+lemma multiset_of_append[simp]: 
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
 
@@ -778,6 +778,9 @@
   apply simp
   done
 
+lemma multiset_of_compl_union[simp]:
+ "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
+  by (induct xs) (auto simp: union_ac)
 
 subsection {* Pointwise ordering induced by count *}