--- 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