# HG changeset patch
# User blanchet
# Date 1432801126 -7200
# Node ID 6b7c64ab8bd234e290932d775757e0ab5cc67f5d
# Parent  7d278b0617d3d109d7225e34eede85489e9ebec3
made Auto Sledgehammer behave more like the real thing

diff -r 7d278b0617d3 -r 6b7c64ab8bd2 NEWS
--- 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)
 ------------------------------
diff -r 7d278b0617d3 -r 6b7c64ab8bd2 src/Doc/Sledgehammer/document/root.tex
--- 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.
 
diff -r 7d278b0617d3 -r 6b7c64ab8bd2 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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,