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/ATP/atp_proof.ML
changeset 41092 1b796ffa8347
parent 40684 c7ba327eb58c
child 41146 be78f4053bce 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 08 22:17:53 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 08 22:17:53 2010 +0100
@@ -109,7 +109,8 @@
   | string_for_failure prover InternalError =
     "An internal " ^ prover ^ " error occurred."
   | string_for_failure prover UnknownError =
-    "An unknown " ^ prover ^ " error occurred."
+    (* "An" is correct for "ATP" and "SMT". *)
+    "An " ^ prover ^ " error occurred."
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
isabelle