--- a/CookBook/Recipes/Timing.thy	Wed Mar 11 17:38:17 2009 +0000
+++ b/CookBook/Recipes/Timing.thy	Wed Mar 11 22:34:49 2009 +0000
@@ -11,18 +11,18 @@
   {\bf Solution:} Time can be measured using the function 
   @{ML start_timing} and @{ML end_timing}.\smallskip
 
-  Assume the following function defined in Isabelle. 
+  Suppose you defined the Ackermann function inside Isabelle. 
 *}
 
 fun 
- ackermann:: "(nat * nat) \<Rightarrow> nat"
+ 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 {* 
-  We can now measure how long the simplifier takes to verify a datapoint
+  You can measure how long the simplifier takes to verify a datapoint
   of this function. The timing can be done using the following wrapper function:
 *}
 
@@ -36,11 +36,13 @@
 end*}
 
 text {*
-  Note that this function also takes a state @{text "st"} as an argument and
-  applies this state to the tactic. This is because tactics are lazy functions
-  and we need to force them to run, otherwise the timing will be meaningless.
-  The used time will be calculated as the end time minus the start time.
-  The wrapper can now be used in the proof
+  Note that this function, in addition to a tactic for which it measures the
+  time, also takes a state @{text "st"} as argument and applies this state to
+  the tactic. 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 for the wrapper is the proof
+
 *}
 
 lemma "ackermann (3, 4) = 125"
@@ -49,7 +51,9 @@
 done
 
 text {*
-  where it returns something on the cale of 3 seconds.
+  where it returns something on the scale of 3 seconds. We choose 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