diff -r 00d153e32a53 -r 3e30ea95c7aa CookBook/Recipes/Timing.thy
--- a/CookBook/Recipes/Timing.thy	Wed Mar 11 13:42:03 2009 +0000
+++ b/CookBook/Recipes/Timing.thy	Wed Mar 11 17:38:17 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Measuring Time\label{rec:timing} (TBD) *} 
+section {* Measuring Time\label{rec:timing} *} 
 
 text {*
  {\bf Problem:}
@@ -11,8 +11,8 @@
   {\bf Solution:} Time can be measured using the function 
   @{ML start_timing} and @{ML end_timing}.\smallskip
 
+  Assume the following function defined in Isabelle. 
 *}
-ML {* timeap *}
 
 fun 
  ackermann:: "(nat * nat) \<Rightarrow> nat"
@@ -21,18 +21,43 @@
   | "ackermann (m, 0) = ackermann (m - 1, 1)"
   | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
 
-text {* Does not work yet! *}
+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
+*}
 
 lemma "ackermann (3, 4) = 125"
-apply(tactic {* timeap  (asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"})) 1 *})
-(*
 apply(tactic {* 
-  let 
-    val start = start_timing ();
-    val res = asm_full_simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1;
-  in
-    (warning (#message  (end_timing start)); res)
-  end *})*)
+  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
 done
 
+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}
+*}
+
+
+
 end
\ No newline at end of file