# HG changeset patch
# User nipkow
# Date 1559291975 -7200
# Node ID 39f5db308fe0525ac47ff927f3dfbe90a39c22a1
# Parent  742f8e7037802b2f870e07e2d3660931fd43a84f
tuned

diff -r 742f8e703780 -r 39f5db308fe0 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Mon May 27 16:47:17 2019 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Fri May 31 10:39:35 2019 +0200
@@ -242,7 +242,7 @@
   qed
 qed
 
-(* Beware of conversions: *)
+(* Beware of implicit conversions: *)
 lemma c_msort_log: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
 using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
 by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
@@ -250,7 +250,6 @@
 
 subsection "Bottom-Up Merge Sort"
 
-(* Exercise: make tail recursive *)
 fun merge_adj :: "('a::linorder) list list \<Rightarrow> 'a list list" where
 "merge_adj [] = []" |
 "merge_adj [xs] = [xs]" |