Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42554 f83036b85a3a
parent 42551 cd99d6d3027a
child 42562 f1d903f789b1 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -972,7 +972,7 @@
            |> kill_useless_labels_in_proof
            |> relabel_proof
            |> string_for_proof ctxt type_sys i n of
-        "" => "\nNo structured proof available."
+        "" => "\nNo structured proof available (proof too short)."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =
       if debug then
isabelle