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.
print a hint
authorblanchet
Tue, 27 Mar 2012 16:59:13 +0300
changeset 47147 bd064bc71085
parent 47146 7276f2b12ff7
child 47148 7b5846065c1b
print a hint
src/HOL/Tools/ATP/atp_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -270,8 +270,12 @@
     val try_line =
       ([], map fst extra)
       |> reconstructor_command reconstr subgoal subgoal_count
-      |> (if failed then enclose "One-line proof reconstruction failed: " "."
-          else try_command_line banner ext_time)
+      |> (if failed then
+            enclose "One-line proof reconstruction failed: "
+                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
+                     \solve this.)"
+          else
+            try_command_line banner ext_time)
   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
 
 (** Hard-core proof reconstruction: structured Isar proofs **)
isabelle