--- a/src/Pure/General/timing.ML Wed Feb 05 13:00:04 2025 +0100
+++ b/src/Pure/General/timing.ML Wed Feb 05 20:46:22 2025 +0100
@@ -16,6 +16,7 @@
sig
include BASIC_TIMING
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+ val zero: timing
type start
val start: unit -> start
val result: start -> timing
@@ -34,6 +35,8 @@
type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
+val zero: timing = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
+
(* timer control *)