diff -r a29b81d4fa88 -r 7c09bd3227c5 CookBook/Recipes/Timing.thy
--- a/CookBook/Recipes/Timing.thy	Fri Mar 13 01:15:55 2009 +0100
+++ b/CookBook/Recipes/Timing.thy	Fri Mar 13 12:21:44 2009 +0100
@@ -23,7 +23,8 @@
 
 text {* 
   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:
+  of this function. The timing of a tactic can be done using the following 
+  wrapper function:
 *}
 
 ML{*fun timing_wrapper tac st =
@@ -36,12 +37,13 @@
 end*}
 
 text {*
-  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
+  Note that this function, in addition to a tactic, 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 of the
+  wrapper is the proof
+
 
 *}