summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Tue, 29 Aug 2017 13:56:15 +0200 | |

changeset 66545 | 97c441c8665d |

parent 66544 | 3e838cf5e80c |

child 66546 | 14a7d2a39336 |

tuned messages

--- 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