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.
prefer explicit
authornipkow
Thu, 13 Sep 2018 08:36:51 +0200
changeset 68985 5d35fd21a0b9
parent 68984 b1d106c1edac
child 68986 22f02724e7d1
child 68988 93546c85374a
prefer explicit
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions
src/HOL/ex/Quicksort.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 06:37:41 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 08:36:51 2018 +0200
@@ -1887,7 +1887,7 @@
 apply simp
 done
 
-lemma mset_compl_union [simp]: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
+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"
--- a/src/HOL/ex/Quicksort.thy	Thu Sep 13 06:37:41 2018 +0200
+++ b/src/HOL/ex/Quicksort.thy	Thu Sep 13 08:36:51 2018 +0200
@@ -22,7 +22,7 @@
 
 lemma quicksort_permutes [simp]:
   "mset (quicksort xs) = mset xs"
-  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
+  by (induct xs rule: quicksort.induct) (simp_all add: mset_compl_union ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
 proof -
isabelle