On Mon, 8 Sep 2014, Lyj238 wrote:
Is there some automatically way to do this time-counting task? I remember that time can be recorded which is used to evaluate an expression.
Larry has already mentioned the Timing panel of Isabelle/jEdit. Some more details on that are in section 4.1 Timing in the Isabelle/jEdit manual, e.g. timing information via tooltips.