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_fact_minimizer.ML
changeset 37418 c02bd0bb276d
parent 36924 ff01d3ae9ad4
child 37479 f6b1ee5b420b 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 14 20:16:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 14 20:48:36 2010 +0200
@@ -38,6 +38,7 @@
 (* wrapper for calling external prover *)
 
 fun string_for_failure Unprovable = "Unprovable."
+  | string_for_failure IncompleteUnprovable = "Failed."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "Failed."
   | string_for_failure OldSpass = "Error."
isabelle