--- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 30 23:52:56 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Jul 30 23:52:56 2014 +0200
@@ -554,26 +554,15 @@
\point{Are generated proofs minimal?}
Automatic provers frequently use many more facts than are necessary.
-Sledgehammer inclues a minimization tool that takes a set of facts returned by a
-given prover and repeatedly calls the same prover, \textit{metis}, or
-\textit{smt2} with subsets of those axioms in order to find a minimal set.
-Reducing the number of axioms typically improves Metis's speed and success rate,
-while also removing superfluous clutter from the proof scripts.
+Sledgehammer includes a minimization tool that takes a set of facts returned by
+a given prover and repeatedly calls a prover or proof method with subsets of
+those facts to find a minimal set. Reducing the number of facts typically helps
+reconstruction, while also removing superfluous clutter from the proof scripts.
In earlier versions of Sledgehammer, generated proofs were systematically
accompanied by a suggestion to invoke the minimization tool. This step is now
-performed implicitly if it can be done in a reasonable amount of time (something
-that can be guessed from the number of facts in the original proof and the time
-it took to find or preplay it).
-
-In addition, some provers do not provide proofs or sometimes produce incomplete
-proofs. The minimizer is then invoked to find out which facts are actually needed
-from the (large) set of facts that was initially given to the prover. Finally,
-if a prover returns a proof with lots of facts, the minimizer is invoked
-automatically since Metis would be unlikely to re-find the proof.
-%
-Automatic minimization can be forced or disabled using the \textit{minimize}
-option (\S\ref{mode-of-operation}).
+performed by default but can be disabled using the \textit{minimize} option
+(\S\ref{mode-of-operation}).
\point{A strange error occurred---what should I do?}
@@ -1008,12 +997,9 @@
\nopagebreak
{\small See also \textit{verbose} (\S\ref{output-format}).}
-\opsmart{minimize}{dont\_minimize}
+\optrue{minimize}{dont\_minimize}
Specifies whether the minimization tool should be invoked automatically after
-proof search. By default, automatic minimization takes place only if
-it can be done in a reasonable amount of time (as determined by
-the number of facts in the original proof and the time it took to find or
-preplay it) or the proof involves an unreasonably large number of facts.
+proof search.
\nopagebreak
{\small See also \textit{preplay\_timeout} (\S\ref{timeouts})