--- a/CookBook/Recipes/TimeLimit.thy	Sun Mar 01 21:48:59 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Mon Mar 02 10:06:06 2009 +0000
@@ -19,6 +19,8 @@
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
+ML {* ackermann (3,4) *} 
+
 text {*
 
   Now the call 

--- a/CookBook/Recipes/Timing.thy	Sun Mar 01 21:48:59 2009 +0000
+++ b/CookBook/Recipes/Timing.thy	Mon Mar 02 10:06:06 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Measuring the Time of an Operation\label{rec:timing} *} 
+section {* Measuring the Time of an Operation\label{rec:timing} (TBD) *} 
 
 text {*
  {\bf Problem:}
@@ -12,23 +12,27 @@
   @{ML start_timing} and @{ML end_timing}.\smallskip
 
 *}
+ML {* timeap *}
 
-ML{*fun ackermann (0, n) = n + 1
-  | ackermann (m, 0) = ackermann (m - 1, 1)
-  | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
+fun 
+ ackermann:: "(nat * 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 {* Does not work yet! *}
 
-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?
-*}
+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 *})*)
+done
 
 end
\ No newline at end of file