Email Gateway (Aug 18 2022 at 20:09): Email Gateway (Aug 18 2022 at 20:09):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi,
I would like to time the processing of individual use_thys command in
the ROOT.ML file.
If I remember correctly, in earlier versions of Isabelle there was a
variant of the use_thy ML commands that returned timing information
(something like time_use_thy?). Is there a replacement or alternative
to achieve the same effect?
I know that with "-t true" I can time the whole session, but I would
like to get a little bit more resolution.
Thank you for your time,
Christoph
Last updated: Apr 20 2024 at 08:16 UTC