--- a/CookBook/FirstSteps.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/FirstSteps.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -897,8 +897,7 @@
    shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
-  application. See Section~\ref{sec:combinators}.}
+  The corresponding ML-code is as follows:
 
 @{ML_response_fake [display,gray]
 "let

--- a/CookBook/Package/Ind_Code.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -553,8 +553,9 @@
   spec_parser >>
     (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*}
 
-ML{*val _ = OuterSyntax.local_theory "simple_inductive" "define inductive predicates"
-          OuterKeyword.thy_decl specification*}
+ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
+              "define inductive predicates"
+                 OuterKeyword.thy_decl specification*}
 
 text {*
   Things to include at the end:

--- a/CookBook/Recipes/Sat.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -104,7 +104,7 @@
 done
 
 text {*
-  However, for prove anything more exciting you have to use a SAT solver
+  However, for proving anything more exciting you have to use a SAT solver
   that can produce a proof. The internal one is not usuable for this. 
 
   \begin{readmore} 

--- a/CookBook/Recipes/Timing.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/Recipes/Timing.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -27,7 +27,7 @@
   wrapper function:
 *}
 
-ML{*fun timing_wrapper tac st =
+ML %linenosgray{*fun timing_wrapper tac st =
 let 
   val t_start = start_timing ();
   val res = tac st;
@@ -38,7 +38,7 @@
 
 text {*
   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
+  "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
@@ -53,7 +53,7 @@
 done
 
 text {*
-  where it returns something on the scale of 3 seconds. We choose to return
+  where it returns something on the scale of 3 seconds. We chose to return
   this information as a string, but the timing information is also accessible
   in number format.
 

Binary file cookbook.pdf has changed