--- 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
@@ -519,7 +519,7 @@
generated by Sledgehammer instead of \textit{metis} if the proof obviously
requires type information or if \textit{metis} failed when Sledgehammer
preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
-various sets of option for up to 2~seconds each time to ensure that the generated
+various sets of option for up to 1~second each time to ensure that the generated
one-line proofs actually work and to display timing information. This can be
configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
options (\S\ref{timeouts}).)
@@ -1373,7 +1373,7 @@
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{preplay\_timeout}{float}{\upshape 2}
+\opdefault{preplay\_timeout}{float}{\upshape 1}
Specifies the maximum number of seconds that \textit{metis} or other proof
methods should spend trying to ``preplay'' the found proof. If this option
is set to 0, no preplaying takes place, and no timing information is displayed
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jul 30 23:52:56 2014 +0200
@@ -97,7 +97,7 @@
("smt_proofs", "smart"),
("slice", "true"),
("minimize", "smart"),
- ("preplay_timeout", "2")]
+ ("preplay_timeout", "1")]
val alias_params =
[("prover", ("provers", [])), (* undocumented *)