diff -r 87f173836d56 -r 503e5280ba72 src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Thu Oct 10 14:13:18 2024 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Sat Oct 12 12:45:29 2024 +0900
@@ -34,16 +34,6 @@
 use \<open>time_function\<close> accompanied by a \<open>termination\<close> command.
 Limitation: The commands do not work properly in locales yet.
 
-If \<open>f\<close> is defined in a type class, one needs to set up a corresponding type class, say \<open>T_f\<close>,
-that fixes a function \<open>T_f\<close> of the corresponding type (ending in type \<open>nat\<close>).
-For every instance of \<open>f :: \<tau>\<close> one needs to create a corresponding instance of the class \<open>T_f\<close>.
-Inside that instance one can now use \<open>time_fun "f :: \<tau>"\<close> to define an instance of the function \<open>T_f\<close>.
-For example, see the definition and instantiation of class \<open>T_size\<close> in theory \<open>Time_Funs\<close>.
-Note that we can just write \<open>time_fun length\<close> because \<open>length\<close> is an abbreviation for \<open>size\<close> on type \<open>list\<close>.
-
-If \<open>f\<close> has an argument of function type, the corresponding argument of \<open>T_f\<close> is a pair
-of that function argument \<open>g\<close> and its corresponding time function \<open>T_g\<close>.
-
 The pre-defined functions below are assumed to have constant running time.
 In fact, we make that constant 0.
 This does not change the asymptotic running time of user-defined functions using the