theory Timing
imports "../Base"
begin

section {* Measuring the Time of an Operation\label{rec:timing} *} 

text {*
 {\bf Problem:}
  You want to measure the running time of a tactic or function.\smallskip

  {\bf Solution:} Time can be measured using the function 
  @{ML start_timing} and @{ML end_timing}.\smallskip

*}

ML{*fun ackermann (0, n) = n + 1
  | ackermann (m, 0) = ackermann (m - 1, 1)
  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}

ML {*
let
  val start = start_timing ()
  val res = ackermann (3,12)
  val time = (end_timing start)
in
 (res,time)
end
*}

text {*
  check what @{text "#all"} does?
*}

end