# HG changeset patch
# User nipkow
# Date 1730906826 -3600
# Node ID 9c47740e974a47d8b1f286aaea7730ba5a7e5758
# Parent  8070e4578ecec4ff326b7627145f54805987d36d
More time for primitive functions

diff -r 8070e4578ece -r 9c47740e974a src/HOL/Data_Structures/Define_Time_Function.thy
--- a/src/HOL/Data_Structures/Define_Time_Function.thy	Wed Nov 06 16:19:45 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.thy	Wed Nov 06 16:27:06 2024 +0100
@@ -49,6 +49,8 @@
 Users of this running time framework need to ensure that 0-time functions are used only
 within the above restrictions.\<close>
 
+time_fun_0 "min"
+time_fun_0 "max"
 time_fun_0 "(+)"
 time_fun_0 "(-)"
 time_fun_0 "(*)"