[isabelle] timing use_thys?



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.