diff -r c22b507e1407 -r e81ebb37aa83 CookBook/Recipes/Timing.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Timing.thy	Sun Mar 01 21:48:59 2009 +0000
@@ -0,0 +1,34 @@
+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
\ No newline at end of file