--- a/src/HOL/Data_Structures/Define_Time_Function.thy Wed Sep 24 16:44:12 2025 +0200
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy Wed Sep 24 17:50:30 2025 +0200
@@ -3,8 +3,7 @@
Automatic definition of step-counting running-time functions from HOL functions
following the translation described in Section 1.5, Running Time, of the book
-Functional Data Structures and Algorithms. A Proof Assistant Approach.
-See https://functional-algorithms-verified.org
+Functional Data Structures and Algorithms. A Proof Assistant Approach. https://fdsa-book.net
*)
theory Define_Time_Function
@@ -33,7 +32,6 @@
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.
The pre-defined functions below are assumed to have constant running time.
In fact, we make that constant 0.