--- a/CookBook/ROOT.ML	Sat Feb 28 14:18:02 2009 +0000
+++ b/CookBook/ROOT.ML	Sun Mar 01 21:48:59 2009 +0000
@@ -17,6 +17,7 @@
 use_thy "Appendix";
 use_thy "Recipes/Antiquotes";
 use_thy "Recipes/TimeLimit";
+use_thy "Recipes/Timing";
 use_thy "Recipes/Config";
 use_thy "Recipes/StoringData";
 use_thy "Recipes/ExternalSolver";

--- a/CookBook/Recipes/Antiquotes.thy	Sat Feb 28 14:18:02 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Sun Mar 01 21:48:59 2009 +0000
@@ -166,8 +166,6 @@
   theorems or cterms.
 
 *}
-
-
 end
   
 

--- a/CookBook/Recipes/Oracle.thy	Sat Feb 28 14:18:02 2009 +0000
+++ b/CookBook/Recipes/Oracle.thy	Sun Mar 01 21:48:59 2009 +0000
@@ -19,7 +19,7 @@
   \begin{readmore}
   A short introduction to oracles can be found in [isar-ref: no suitable label
   for section 3.11]. A simple example, which we will slightly extend here,
-  is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding
+  is given in @{ML_file "FOL/ex/Iff_Oracle.thy"}. The raw interface for adding
   oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.
   \end{readmore}
 

--- /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

Binary file cookbook.pdf has changed