--- a/ProgTutorial/Recipes/Sat.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Recipes/Sat.thy	Wed May 28 12:41:09 2014 +0100
@@ -66,35 +66,30 @@
   to see better which assignment the table contains.
  
   Having produced a propositional formula, you can now call the SAT solvers 
-  with the function @{ML "SatSolver.invoke_solver"}. For example
+  with the function @{ML "SAT_Solver.invoke_solver"}. For example
 
   @{ML_response_fake [display,gray]
-  "SatSolver.invoke_solver \"dpll\" pform"
-  "SatSolver.SATISFIABLE assg"}
+  "SAT_Solver.invoke_solver \"minisat\" pform"
+  "SAT_Solver.SATISFIABLE assg"}
 
   determines that the formula @{ML pform} is satisfiable. If we inspect
   the returned function @{text assg}
 
   @{ML_response [display,gray]
 "let
-  val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
+  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
 in 
   (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"}
+  we obtain a possible assignment for the variables @{text "A"} an @{text "B"}
   that makes the formula satisfiable. 
 
-  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\" pform"}
-
+  Note that we invoked the SAT solver with the string @{text [quotes] auto}. 
+  This string specifies which specific SAT solver is invoked. If instead 
+  called with @{text [quotes] "auto"}
   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 SAT solvers. One 
   is the tactic @{ML sat_tac in SAT}. For example