diff -r 8bb4eaa2ec92 -r c7f04a008c9c CookBook/Recipes/Sat.thy
--- a/CookBook/Recipes/Sat.thy	Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/Recipes/Sat.thy	Wed Mar 18 03:03:51 2009 +0100
@@ -16,79 +16,86 @@
   is based on the DPLL algorithm.\smallskip
 
   The SAT solvers expect a propositional formula as input and produce
-  a result indicating that the formula is satisfiable, unsatisfiable or
+  a result indicating that the formula is either satisfiable, unsatisfiable or
   unknown. The type of the propositional formula is  
   @{ML_type "PropLogic.prop_formula"} with the usual constructors such 
   as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.
 
-  There is the function  @{ML  PropLogic.prop_formula_of_term}, which
-  translates an Isabelle term into a propositional formula. Let
-  us illustrate this function with translating the term @{term "A \<and> \<not>A \<or> B"}. 
-  Suppose the ML-value
+  The function  @{ML  PropLogic.prop_formula_of_term} translates an Isabelle 
+  term into a propositional formula. Let
+  us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. 
+  The function will return a propositional formula and a table. Suppose 
 *}
 
-ML{*val (form, tab) = 
+ML{*val (pform, table) = 
        PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
 
 text {*
-  then the resulting propositional formula @{ML form} is 
-  @{ML "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 
-  where indices are assigned  for the propositional variables 
-  @{text "A"} and @{text "B"} respectively. This assignment is recorded 
+  then the resulting propositional formula @{ML pform} is 
+  
+  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 
+  
+
+  where indices are assigned for the variables 
+  @{text "A"} and @{text "B"}, respectively. This assignment is recorded 
   in the table that is given to the translation function and also returned 
   (appropriately updated) in the result. In the case above the
-  input table is empty and the output table is
+  input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
 
   @{ML_response_fake [display,gray]
-  "Termtab.dest tab"
+  "Termtab.dest table"
   "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
 
-  A propositional variable is also introduced whenever the translation
+  An index is also produced whenever the translation
   function cannot find an appropriate propositional formula for a term. 
-  Given the ML-value
+  Attempting to translate @{term "\<forall>x::nat. P x"}
 *}
 
-ML{*val (form', tab') = 
+ML{*val (pform', table') = 
        PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
 
 text {*
-  @{ML form'} is now the propositional variable @{ML "BoolVar 1" in PropLogic} 
-  and the table @{ML tab'} is
+  returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 
+  @{ML table'} is:
 
   @{ML_response_fake [display,gray]
-  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest tab')"
+  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
   "(\<forall>x. P x, 1)"}
   
-  Having produced a propositional formula, you can call the SAT solvers 
-  with the function @{ML "SatSolver.invoke_solver"}. 
-  For example
+  We used some pretty printing scaffolding to see better what the output is.
+ 
+  Having produced a propositional formula, you can now call the SAT solvers 
+  with the function @{ML "SatSolver.invoke_solver"}. For example
 
   @{ML_response_fake [display,gray]
-  "SatSolver.invoke_solver \"dpll\" form"
-  "SatSolver.SATISFIABLE ass"}
+  "SatSolver.invoke_solver \"dpll\" pform"
+  "SatSolver.SATISFIABLE assg"}
 
-  determines that the formula @{ML form} is satisfiable. If we inspect
-  the returned function @{text ass}
+  determines that the formula @{ML pform} is satisfiable. If we inspect
+  the returned function @{text assg}
 
   @{ML_response [display,gray]
 "let
-  val SatSolver.SATISFIABLE ass = SatSolver.invoke_solver \"dpll\" form
+  val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
 in 
-  (ass 1, ass 2, ass 3)
+  (assg 1, assg 2, assg 3)
 end"
   "(SOME true, SOME true, NONE)"}
 
   we obtain a possible assignment for the variables @{text "A"} and @{text "B"}
   that makes the formula satisfiable. 
 
-  If we instead invoke the SAT solver with the string @{text [quotes] "auto"}
+  Note that we invoked the SAT solver with the string @{text [quotes] dpll}. 
+  This string specifies which SAT solver is invoked (in this case the internal
+  one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}
 
-  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" form"}
+  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}
 
-  several external SAT solvers will be tried (if they are installed) and
-  the default is the internal SAT solver @{text [quotes] "dpll"}.
+  several external SAT solvers will be tried (assuming they are installed). 
+  If no external SAT solver is installed, then the default is 
+  @{text [quotes] "dpll"}.
 
-  There are also two tactics that make use of the SAT solvers. One 
+  There are also two tactics that make use of SAT solvers. One 
   is the tactic @{ML sat_tac in sat}. For example 
 *}
 
@@ -97,6 +104,9 @@
 done
 
 text {*
+  However, for prove 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} 
   The interface for the external SAT solvers is implemented
   in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple