--- a/src/HOL/Data_Structures/Selection.thy Fri Aug 23 18:40:12 2024 +0200
+++ b/src/HOL/Data_Structures/Selection.thy Mon Aug 26 18:26:00 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