--- a/ProgTutorial/Recipes/Timing.thy	Thu Mar 19 17:50:28 2009 +0100
+++ b/ProgTutorial/Recipes/Timing.thy	Thu Mar 19 23:21:26 2009 +0100
@@ -11,7 +11,7 @@
   {\bf Solution:} Time can be measured using the function 
   @{ML start_timing} and @{ML end_timing}.\smallskip
 
-  Suppose you defined the Ackermann function inside Isabelle. 
+  Suppose you defined the Ackermann function on the Isabelle level. 
 *}
 
 fun 
@@ -23,7 +23,7 @@
 
 text {* 
   You can measure how long the simplifier takes to verify a datapoint
-  of this function. The timing of a tactic can be done using the following 
+  of this function. The actual timing is done inside the
   wrapper function:
 *}
 
@@ -40,11 +40,14 @@
   Note that this function, in addition to a tactic, also takes a state @{text
   "st"} as argument and applies this state to the tactic (Line 4). 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 of the
+  timing will be meaningless. The simplifier tactic, amongst others,  can be 
+  forced to run by just applying the state to it. But ``fully'' lazy tactics,
+  such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force
+  them to run. 
+
+  The time between start and finish of the simplifier will be calculated 
+  as the end time minus the start time.  An example of the
   wrapper is the proof
-
-
 *}
 
 lemma "ackermann (3, 4) = 125"