merged
authornipkow
Mon, 26 Aug 2024 18:26:06 +0200 (4 months ago)
changeset 80775 de95c82eb31a
parent 80773 83d21da2bc59 (current diff)
parent 80774 a2486a4b42da (diff)
child 80776 3a9e570c916d
merged
--- a/src/HOL/Data_Structures/Selection.thy	Mon Aug 26 13:15:34 2024 +0200
+++ b/src/HOL/Data_Structures/Selection.thy	Mon Aug 26 18:26:06 2024 +0200
@@ -633,9 +633,7 @@
 
 subsection \<open>Running time analysis\<close>
 
-fun T_partition3 :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
-  "T_partition3 x [] = 1"
-| "T_partition3 x (y # ys) = T_partition3 x ys + 1"
+time_fun partition3 equations partition3_code
 
 lemma T_partition3_eq: "T_partition3 x xs = length xs + 1"
   by (induction x xs rule: T_partition3.induct) auto