# HG changeset patch
# User blanchet
# Date 1381843892 -7200
# Node ID 84791e3fdcdeedca7f08eef1b7d0d9cca9a08448
# Parent  df080dfefddc7d17becc0ffe00d0bb106c647c35
updated S/H docs

diff -r df080dfefddc -r 84791e3fdcde src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Oct 15 15:31:18 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Oct 15 15:31:32 2013 +0200
@@ -121,8 +121,8 @@
 
 For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be
 enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options >
-Isabelle > General.'' In this mode, Sledgehammer is run on every newly entered
-theorem.
+Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
+every newly entered theorem for a few seconds.
 
 \newbox\boxA
 \setbox\boxA=\hbox{\texttt{NOSPAM}}
@@ -719,12 +719,16 @@
 If you use Isabelle/jEdit, Sledgehammer also provides an automatic mode that can
 be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options
 > Isabelle > General.'' For automatic runs, only the first prover set using
-\textit{provers} (\S\ref{mode-of-operation}) is considered, fewer facts are
-passed to the prover, \textit{slice} (\S\ref{mode-of-operation}) is disabled,
-\textit{strict} (\S\ref{problem-encoding}) is enabled, \textit{verbose}
-(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
-and \textit{timeout} (\S\ref{timeouts}) is superseded by the ``Auto Time Limit''
-option in jEdit. Sledgehammer's output is also more concise.
+\textit{provers} (\S\ref{mode-of-operation}) is considered (typically E),
+\textit{slice} (\S\ref{mode-of-operation}) is disabled,
+\textit{minimize} (\S\ref{mode-of-operation}) is disabled, fewer facts are
+passed to the prover, \textit{fact\_filter} (\S\ref{relevance-filter}) is set to
+\textit{mepo}, \textit{strict} (\S\ref{problem-encoding}) is enabled,
+\textit{verbose} (\S\ref{output-format}) and \textit{debug}
+(\S\ref{output-format}) are disabled, \textit{preplay\_timeout}
+(\S\ref{timeouts}) is set to 0, and \textit{timeout} (\S\ref{timeouts}) is
+superseded by the ``Auto Time Limit'' option in jEdit. Sledgehammer's output is
+also more concise.
 
 \subsection{Metis}
 
@@ -999,8 +1003,7 @@
 number of facts. For SMT solvers, several slices are tried with the same options
 each time but fewer and fewer facts. According to benchmarks with a timeout of
 30 seconds, slicing is a valuable optimization, and you should probably leave it
-enabled unless you are conducting experiments. This option is implicitly
-disabled for (short) automatic runs.
+enabled unless you are conducting experiments.
 
 \nopagebreak
 {\small See also \textit{verbose} (\S\ref{output-format}).}
@@ -1282,14 +1285,12 @@
 
 \opfalse{verbose}{quiet}
 Specifies whether the \textbf{sledgehammer} command should explain what it does.
-This option is implicitly disabled for automatic runs.
 
 \opfalse{debug}{no\_debug}
 Specifies whether Sledgehammer should display additional debugging information
 beyond what \textit{verbose} already displays. Enabling \textit{debug} also
 enables \textit{verbose} and \textit{blocking} (\S\ref{mode-of-operation})
-behind the scenes. The \textit{debug} option is implicitly disabled for
-automatic runs.
+behind the scenes.
 
 \nopagebreak
 {\small See also \textit{spy} (\S\ref{mode-of-operation}) and
@@ -1349,8 +1350,6 @@
 \opdefault{timeout}{float\_or\_none}{\upshape 30}
 Specifies the maximum number of seconds that the automatic provers should spend
 searching for a proof. This excludes problem preparation and is a soft limit.
-For automatic runs, the ``Auto Time Limit'' option under ``Plugins > Plugin
-Options > Isabelle > General'' is used instead.
 
 \opdefault{preplay\_timeout}{float\_or\_none}{\upshape 3}
 Specifies the maximum number of seconds that \textit{metis} or \textit{smt}