# HG changeset patch
# User nipkow
# Date 1536848105 -7200
# Node ID a319e3c522ba44d9c7842c8dc4219eabc5b18e02
# Parent  d6d5fb521896d649d2e2e88800fd5581cb7d5c1c
removed redundant lemma

diff -r d6d5fb521896 -r a319e3c522ba src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 15:15:50 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 16:15:05 2018 +0200
@@ -1890,9 +1890,6 @@
 lemma union_mset_compl[simp]: "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
 by (induction M) simp_all
 
-lemma mset_compl_union: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
-  by (induct xs) auto
-
 lemma nth_mem_mset: "i < length ls \<Longrightarrow> (ls ! i) \<in># mset ls"
 proof (induct ls arbitrary: i)
   case Nil
diff -r d6d5fb521896 -r a319e3c522ba src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Thu Sep 13 15:15:50 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy	Thu Sep 13 16:15:05 2018 +0200
@@ -22,7 +22,7 @@
 
 lemma quicksort_permutes [simp]:
   "mset (quicksort xs) = mset xs"
-  by (induct xs rule: quicksort.induct) (simp_all add: mset_compl_union ac_simps)
+by (induction xs rule: quicksort.induct) (simp_all)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
 proof -