--- a/src/HOL/Data_Structures/Define_Time_Function.thy Thu Aug 22 22:26:36 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy Fri Aug 23 18:40:12 2024 +0200
@@ -34,6 +34,16 @@
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