--- a/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Jan 31 16:09:23 2022 +0100
@@ -561,8 +561,8 @@
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 (typically E),
-\textit{slice} (\S\ref{timeouts}) is set to 0, fewer facts are
+\textit{provers} (\S\ref{mode-of-operation}) is considered,
+\textit{dont\_slice} (\S\ref{timeouts}) is set, 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}
@@ -1180,19 +1180,20 @@
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.
-\opdefault{slice}{float}{\upshape 5}
-Specifies the size of the time slices for each invocation of a prover. Each time
-slice has its own set of options. For example, for SPASS, the first slice might
-try the fast but incomplete set-of-support strategy, whereas other slices might
-run without it. Slicing can be disable by setting \textit{slice} to 0. However,
-slicing is a valuable optimization, and you should probably leave it enabled
-unless you are conducting experiments.
+\opdefault{slices}{int}{\upshape 6 times the number of cores detected}
+Specifies the number of time slices. Each time slice corresponds to a prover
+invocation and has its own set of options. For example, for SPASS, one slice
+might specify the fast but incomplete set-of-support (SOS) strategy with 100
+relevant lemmas, whereas other slices might run without SOS and with 500 lemmas.
+Slicing (and thereby parallelism) can be disable by setting \textit{slices} to
+1. Since slicing is a valuable optimization, you should probably leave it
+enabled unless you are conducting experiments.
\nopagebreak
{\small See also \textit{verbose} (\S\ref{output-format}).}
\optrueonly{dont\_slice}
-Alias for ``\textit{slice} = 0''.
+Alias for ``\textit{slices} = 1''.
\opdefault{preplay\_timeout}{float}{\upshape 1}
Specifies the maximum number of seconds that \textit{metis} or other proof