# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID e9e27d2e61a1868ae754e4c5a8e2341f8aabacd6
# Parent  75718e81554c77d3f0a41b23015c7e56a93b5139
updated documentation of 'slice' (now 'slices') option

diff -r 75718e81554c -r e9e27d2e61a1 src/Doc/Sledgehammer/document/root.tex
--- 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