doc-src/Nitpick/nitpick.tex
changeset 33229 fba7527c3ef1
parent 33196 5fe67e108651
child 33232 f93390060bbe
--- a/doc-src/Nitpick/nitpick.tex	Mon Oct 26 14:57:49 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Oct 26 18:52:16 2009 +0100
@@ -2091,11 +2091,11 @@
 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
 
 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
-\textit{smart}, Nitpick selects the first solver among MiniSat, PicoSAT, zChaff,
-RSat, BerkMin, BerkMinAlloy, and Jerusat that is recognized by Isabelle. If none
-is found, it falls back on SAT4J, which should always be available. If
-\textit{verbose} is enabled, Nitpick displays which SAT solver was chosen.
-
+\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat,
+PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is
+recognized by Isabelle. If none is found, it falls back on SAT4J, which should
+always be available. If \textit{verbose} is enabled, Nitpick displays which SAT
+solver was chosen.
 \end{enum}
 \fussy