# HG changeset patch
# User nipkow
# Date 1724689566 -7200
# Node ID de95c82eb31ac76c95185725bbb4a84758a1d729
# Parent  83d21da2bc594e0ab7f4290e479e7a343f0a956e# Parent  a2486a4b42da3770e53e7996880c786c3ace8342
merged

diff -r 83d21da2bc59 -r de95c82eb31a src/HOL/Data_Structures/Selection.thy
--- 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