section {* Measuring Time\label{rec:timing} *} 

  Assume the following function defined in Isabelle. 

text {* 

  We can now measure how long the simplifier takes to verify a datapoint

  of this function. The timing can be done using the following wrapper function:

*}

ML{*fun timing_wrapper tac st =

let 

  val t_start = start_timing ();

  val res = tac st;

  val t_end = end_timing t_start;

in

  (warning (#message t_end); res)

end*}

text {*

  Note that this function also takes a state @{text "st"} as an argument and

  applies this state to the tactic. This is because tactics are lazy functions

  and we need to force them to run, otherwise the timing will be meaningless.

  The used time will be calculated as the end time minus the start time.

  The wrapper can now be used in the proof

*}

  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})

text {*

  where it returns something on the cale of 3 seconds.

  \begin{readmore}

  Basic functions regarding timing are defined in @{ML_file 

  "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more

  advanced functions are defined in @{ML_file "Pure/General/output.ML"}.

  \end{readmore}

*}