src/HOL/Data_Structures/Define_Time_Function.thy

 running time functions must already have been defined.
 If the definition of the function requires a manual termination proof,
 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
 pre-defined functions because 1 is added for every user-defined function call.