Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed hint that is seldom useful in practice
authorblanchet
Thu, 13 Feb 2014 13:16:16 +0100
changeset 55451 ea1d9408a233
parent 55450 9eddc17749f7
child 55452 29ec8680e61f
removed hint that is seldom useful in practice
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 12:24:28 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:16 2014 +0100
@@ -183,11 +183,8 @@
     val try_line =
       map fst extra
       |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
-      |> (if failed then
-            enclose "One-line proof reconstruction failed: "
-              ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
-          else
-            try_command_line banner ext_time)
+      |> (if failed then enclose "One-line proof reconstruction failed: " "."
+          else try_command_line banner ext_time)
   in
     try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   end
isabelle