diff -r ca0ac2e75f6d -r 0150cf5982ae ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Thu Mar 19 17:50:28 2009 +0100
+++ b/ProgTutorial/Recipes/Sat.thy	Thu Mar 19 23:21:26 2009 +0100
@@ -62,7 +62,8 @@
   "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
   "(\<forall>x. P x, 1)"}
   
-  We used some pretty printing scaffolding to see better what the output is.
+  In the print out of the tabel, we used some pretty printing scaffolding 
+  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
@@ -104,8 +105,9 @@
 done
 
 text {*
-  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. 
+  However, for proving anything more exciting using @{ML "sat_tac" in sat} 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