# HG changeset patch
# User nipkow
# Date 1724431212 -7200
# Node ID 6adf6cc82013288577404bd218415ad8a7f63880
# Parent  6984640568b94c9084405e9882278b11f73d79f5
tuned comments

diff -r 6984640568b9 -r 6adf6cc82013 src/HOL/Data_Structures/Define_Time_Function.thy
--- 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