# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237286821 -3600
# Node ID 5baaabe1ab9206f4ff41606e4f859c647c793f95
# Parent  9c25418db6f0273d316ce25d4c81385e9d814399
updated to new method_setup

diff -r 9c25418db6f0 -r 5baaabe1ab92 CookBook/Intro.thy
--- 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:
diff -r 9c25418db6f0 -r 5baaabe1ab92 CookBook/Parsing.thy
--- 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 
diff -r 9c25418db6f0 -r 5baaabe1ab92 CookBook/Recipes/Oracle.thy
--- 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:
 *}
 
diff -r 9c25418db6f0 -r 5baaabe1ab92 CookBook/Recipes/Sat.thy
--- 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}
 *}
diff -r 9c25418db6f0 -r 5baaabe1ab92 cookbook.pdf
Binary file cookbook.pdf has changed