--- a/src/HOL/Data_Structures/Sorting.thy Wed May 09 23:31:11 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy Thu May 10 01:34:07 2018 +0200
@@ -306,17 +306,17 @@
subsubsection "Time Complexity"
-fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> real" where
+fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
"c_merge_adj [] = 0" |
"c_merge_adj [x] = 0" |
"c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs"
-fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where
+fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
"c_merge_all [] = undefined" |
"c_merge_all [x] = 0" |
"c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)"
-definition c_msort_bu :: "('a::linorder) list \<Rightarrow> real" where
+definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
"c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
lemma length_merge_adj: