--- 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
--- 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 -