# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1235944139 0
# Node ID e81ebb37aa83f262fd705a7897ba1adc742932bb
# Parent  c22b507e1407c17ff39b81d8f411dc84235d8a41
updated to repository version; added a section about timing

diff -r c22b507e1407 -r e81ebb37aa83 CookBook/ROOT.ML
--- 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";
diff -r c22b507e1407 -r e81ebb37aa83 CookBook/Recipes/Antiquotes.thy
--- 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
   
 
diff -r c22b507e1407 -r e81ebb37aa83 CookBook/Recipes/Oracle.thy
--- 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}
 
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
diff -r c22b507e1407 -r e81ebb37aa83 cookbook.pdf
Binary file cookbook.pdf has changed