# HG changeset patch
# User nipkow
# Date 1525908827 -7200
# Node ID cba8eaa2174f954b2308485b9b09f5e018b3a5d8
# Parent  2e5b737810a60a9f504f9c7f4168b3433d71a9c4
simpler types

diff -r 2e5b737810a6 -r cba8eaa2174f src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Wed May 09 07:48:54 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Thu May 10 01:33:47 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: