--- a/NEWS Thu May 28 09:50:17 2015 +0200
+++ b/NEWS Thu May 28 10:18:46 2015 +0200
@@ -10,6 +10,11 @@
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
+* Sledgehammer:
+ - Proof reconstruction has been improved, to minimize the incidence of
+ cases where Sledgehammer gives a proof that does not work.
+ - Auto Sledgehammer now minimizes and preplays the results.
+
New in Isabelle2015 (May 2015)
------------------------------
--- a/src/Doc/Sledgehammer/document/root.tex Thu May 28 09:50:17 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu May 28 10:18:46 2015 +0200
@@ -667,12 +667,11 @@
> 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{mode-of-operation}) is disabled,
-\textit{minimize} (\S\ref{mode-of-operation}) is disabled, fewer facts are
+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
+(\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.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu May 28 09:50:17 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu May 28 10:18:46 2015 +0200
@@ -275,9 +275,9 @@
val try0 = lookup_bool "try0"
val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
- val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
+ val minimize = lookup_bool "minimize"
val timeout = lookup_time "timeout"
- val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
+ val preplay_timeout = lookup_time "preplay_timeout"
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,