--- a/src/HOL/Data_Structures/Sorting.thy Mon Sep 10 15:08:56 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy Mon Sep 10 20:48:22 2018 +0200
@@ -273,7 +273,7 @@
"\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)"
by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
-lemma msec_merge_all:
+lemma mset_merge_all:
"xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))"
by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj)
@@ -290,7 +290,7 @@
by(simp add: msort_bu_def sorted_merge_all)
lemma mset_msort_bu: "mset (msort_bu xs) = mset xs"
-by(simp add: msort_bu_def msec_merge_all comp_def)
+by(simp add: msort_bu_def mset_merge_all comp_def)
subsubsection "Time Complexity"