# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237343235 -3600
# Node ID 043ef82000b49363a9b9dae991f5e5bfbbe48186
# Parent  c7f04a008c9c1d7a35c770df88a2cf6648204024
some polishing

diff -r c7f04a008c9c -r 043ef82000b4 CookBook/FirstSteps.thy
--- 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
diff -r c7f04a008c9c -r 043ef82000b4 CookBook/Package/Ind_Code.thy
--- 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:
diff -r c7f04a008c9c -r 043ef82000b4 CookBook/Recipes/Sat.thy
--- 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} 
diff -r c7f04a008c9c -r 043ef82000b4 CookBook/Recipes/Timing.thy
--- 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.
 
diff -r c7f04a008c9c -r 043ef82000b4 cookbook.pdf
Binary file cookbook.pdf has changed