# HG changeset patch
# User nipkow
# Date 1525908847 -7200
# Node ID 9339687ca07193deb8b3c8e925dcbb1831a5a1de
# Parent  763f5a8f3f7f01c87cd287219302f5957c359aa9# Parent  cba8eaa2174f954b2308485b9b09f5e018b3a5d8
merged

diff -r 763f5a8f3f7f -r 9339687ca071 src/HOL/Data_Structures/Sorting.thy
--- 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: