--- a/CookBook/Intro.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Intro.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -60,7 +60,8 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  to learn from that code.
+  to learn from that code. The UNIX command @{text "grep -R"} is
+  often your best friend while programming with Isabelle. 
   \end{description}
 
 *}
@@ -69,7 +70,7 @@
 
 text {*
 
-  All ML-code in this tutorial is typeset in highlighted boxes, like the following 
+  All ML-code in this tutorial is typeset in shaded boxes, like the following 
   ML-expression:
 
   \begin{isabelle}
@@ -96,10 +97,10 @@
 
   The user-level commands of Isabelle (i.e.~the non-ML code) are written
   in bold, for example \isacommand{lemma}, \isacommand{apply},
-  \isacommand{foobar} and so on.  We use @{text "$"} to indicate that a
+  \isacommand{foobar} and so on.  We use @{text "$ \<dots>"} to indicate that a
   command needs to be run in a Unix-shell, for example:
 
-  @{text [display] "$ ls -la"}
+  @{text [display] "$ grep -R ThyOutput *"}
 
   Pointers to further information and Isabelle files are typeset in 
   italic and highlighted as follows:

--- a/CookBook/Parsing.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Parsing.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -993,9 +993,9 @@
 *}
 
 method_setup %gray foobar_meth = 
- {* Method.no_args 
-      (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
-        "foobar method"
+ {* Scan.succeed
+      (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
+         "foobar method"
 
 text {*
   It defines the method @{text foobar_meth} which takes no arguments and 

--- a/CookBook/Recipes/Oracle.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Recipes/Oracle.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -133,12 +133,10 @@
 *}
 
 method_setup iff_oracle = {*
-   Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)
+   Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
 *} "Oracle-based decision procedure for chains of equivalences"
 
 text {*
-  (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?)
-
   Finally, we can test our oracle to prove some theorems:
 *}
 

--- a/CookBook/Recipes/Sat.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -3,7 +3,7 @@
 imports Main "../Base"
 begin
 
-section {* SAT Solver\label{rec:sat} *}
+section {* SAT Solvers\label{rec:sat} *}
 
 text {*
   {\bf Problem:}
@@ -101,9 +101,9 @@
   The interface for the external SAT solvers is implemented
   in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple
   SAT solver based on the DPLL algorithm. The tactics for SAT solvers are
-  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"} Functions concerning
+  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning
   propositional formulas are implemented in @{ML_file
-  "HOL/Tools/prop_logic.ML"}. Tables used in the translation function are
+  "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
   implemented in @{ML_file "Pure/General/table.ML"}.  
   \end{readmore}
 *}

Binary file cookbook.pdf has changed