--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 13:56:14 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 13:56:15 2017 +0200
@@ -173,45 +173,43 @@
""
val missing_message_tail =
- " appears to be missing. You will need to install it if you want to invoke \
- \remote provers."
+ " appears to be missing; you will need to install it if you want to invoke \
+ \remote provers"
fun from_lemmas [] = ""
| from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss))
-fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable."
- | string_of_atp_failure Unprovable = "The generated problem is unprovable."
- | string_of_atp_failure GaveUp = "The prover gave up."
+fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable"
+ | string_of_atp_failure Unprovable = "The generated problem is unprovable"
+ | string_of_atp_failure GaveUp = "The prover gave up"
| string_of_atp_failure ProofMissing =
- "The prover claims the conjecture is a theorem but did not provide a proof."
+ "The prover claims the conjecture is a theorem but did not provide a proof"
| string_of_atp_failure ProofIncomplete =
- "The prover claims the conjecture is a theorem but provided an incomplete proof."
+ "The prover claims the conjecture is a theorem but provided an incomplete proof"
| string_of_atp_failure ProofUnparsable =
- "The prover claims the conjecture is a theorem but provided an unparsable proof."
+ "The prover claims the conjecture is a theorem but provided an unparsable proof"
| string_of_atp_failure (UnsoundProof (false, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ". Specify a sound type encoding or omit the \"type_enc\" option."
+ "; specify a sound type encoding or omit the \"type_enc\" option"
| string_of_atp_failure (UnsoundProof (true, ss)) =
"The prover derived \"False\"" ^ from_lemmas ss ^
- ", which could be due to inconsistent axioms (including \"sorry\"s) or to \
- \a bug in Sledgehammer."
- | string_of_atp_failure CantConnect = "Cannot connect to server."
- | string_of_atp_failure TimedOut = "Timed out."
+ ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)"
+ | string_of_atp_failure CantConnect = "Cannot connect to server"
+ | string_of_atp_failure TimedOut = "Timed out"
| string_of_atp_failure Inappropriate =
- "The generated problem lies outside the prover's scope."
- | string_of_atp_failure OutOfResources = "The prover ran out of resources."
+ "The generated problem lies outside the prover's scope"
+ | string_of_atp_failure OutOfResources = "The prover ran out of resources"
| string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail
| string_of_atp_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_of_atp_failure MalformedInput = "The generated problem is malformed."
- | string_of_atp_failure MalformedOutput = "The prover output is malformed."
- | string_of_atp_failure Interrupted = "The prover was interrupted."
- | string_of_atp_failure Crashed = "The prover crashed."
- | string_of_atp_failure InternalError = "An internal prover error occurred."
+ | string_of_atp_failure MalformedInput = "The generated problem is malformed"
+ | string_of_atp_failure MalformedOutput = "The prover output is malformed"
+ | string_of_atp_failure Interrupted = "The prover was interrupted"
+ | string_of_atp_failure Crashed = "The prover crashed"
+ | string_of_atp_failure InternalError = "An internal prover error occurred"
| string_of_atp_failure (UnknownError s) =
"A prover error occurred" ^
- (if s = "" then ". (Pass the \"verbose\" option for details.)"
- else ":\n" ^ s)
+ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s)
fun extract_delimited (begin_delim, end_delim) output =
(case first_field begin_delim output of