--- a/CookBook/Recipes/Timing.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-theory Timing
-imports "../Base"
-begin
-
-section {* Measuring Time\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
-
-  Suppose you defined the Ackermann function inside Isabelle. 
-*}
-
-fun 
- ackermann:: "(nat \<times> nat) \<Rightarrow> nat"
-where
-    "ackermann (0, n) = n + 1"
-  | "ackermann (m, 0) = ackermann (m - 1, 1)"
-  | "ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1))"
-
-text {* 
-  You can measure how long the simplifier takes to verify a datapoint
-  of this function. The timing of a tactic can be done using the following 
-  wrapper function:
-*}
-
-ML %linenosgray{*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, in addition to a tactic, also takes a state @{text
-  "st"} as argument and applies this state to the tactic (Line 4). The reason is that
-  tactics are lazy functions and you need to force them to run, otherwise the
-  timing will be meaningless.  The time between start and finish of the tactic
-  will be calculated as the end time minus the start time.  An example of the
-  wrapper is the proof
-
-
-*}
-
-lemma "ackermann (3, 4) = 125"
-apply(tactic {* 
-  timing_wrapper (simp_tac (@{simpset} addsimps @{thms "nat_number"}) 1) *})
-done
-
-text {*
-  where it returns something on the scale of 3 seconds. We chose to return
-  this information as a string, but the timing information is also accessible
-  in number format.
-
-  \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