summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Tools/ATP/atp_proof.ML

changeset 66545 | 97c441c8665d |

parent 66544 | 3e838cf5e80c |

child 67021 | 41f1f8c4259b |

1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 13:56:14 2017 +0200 1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 29 13:56:15 2017 +0200 1.3 @@ -173,45 +173,43 @@ 1.4 "" 1.5 1.6 val missing_message_tail = 1.7 - " appears to be missing. You will need to install it if you want to invoke \ 1.8 - \remote provers." 1.9 + " appears to be missing; you will need to install it if you want to invoke \ 1.10 + \remote provers" 1.11 1.12 fun from_lemmas [] = "" 1.13 | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) 1.14 1.15 -fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable." 1.16 - | string_of_atp_failure Unprovable = "The generated problem is unprovable." 1.17 - | string_of_atp_failure GaveUp = "The prover gave up." 1.18 +fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable" 1.19 + | string_of_atp_failure Unprovable = "The generated problem is unprovable" 1.20 + | string_of_atp_failure GaveUp = "The prover gave up" 1.21 | string_of_atp_failure ProofMissing = 1.22 - "The prover claims the conjecture is a theorem but did not provide a proof." 1.23 + "The prover claims the conjecture is a theorem but did not provide a proof" 1.24 | string_of_atp_failure ProofIncomplete = 1.25 - "The prover claims the conjecture is a theorem but provided an incomplete proof." 1.26 + "The prover claims the conjecture is a theorem but provided an incomplete proof" 1.27 | string_of_atp_failure ProofUnparsable = 1.28 - "The prover claims the conjecture is a theorem but provided an unparsable proof." 1.29 + "The prover claims the conjecture is a theorem but provided an unparsable proof" 1.30 | string_of_atp_failure (UnsoundProof (false, ss)) = 1.31 "The prover derived \"False\"" ^ from_lemmas ss ^ 1.32 - ". Specify a sound type encoding or omit the \"type_enc\" option." 1.33 + "; specify a sound type encoding or omit the \"type_enc\" option" 1.34 | string_of_atp_failure (UnsoundProof (true, ss)) = 1.35 "The prover derived \"False\"" ^ from_lemmas ss ^ 1.36 - ", which could be due to inconsistent axioms (including \"sorry\"s) or to \ 1.37 - \a bug in Sledgehammer." 1.38 - | string_of_atp_failure CantConnect = "Cannot connect to server." 1.39 - | string_of_atp_failure TimedOut = "Timed out." 1.40 + ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" 1.41 + | string_of_atp_failure CantConnect = "Cannot connect to server" 1.42 + | string_of_atp_failure TimedOut = "Timed out" 1.43 | string_of_atp_failure Inappropriate = 1.44 - "The generated problem lies outside the prover's scope." 1.45 - | string_of_atp_failure OutOfResources = "The prover ran out of resources." 1.46 + "The generated problem lies outside the prover's scope" 1.47 + | string_of_atp_failure OutOfResources = "The prover ran out of resources" 1.48 | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail 1.49 | string_of_atp_failure NoLibwwwPerl = 1.50 "The Perl module \"libwww-perl\"" ^ missing_message_tail 1.51 - | string_of_atp_failure MalformedInput = "The generated problem is malformed." 1.52 - | string_of_atp_failure MalformedOutput = "The prover output is malformed." 1.53 - | string_of_atp_failure Interrupted = "The prover was interrupted." 1.54 - | string_of_atp_failure Crashed = "The prover crashed." 1.55 - | string_of_atp_failure InternalError = "An internal prover error occurred." 1.56 + | string_of_atp_failure MalformedInput = "The generated problem is malformed" 1.57 + | string_of_atp_failure MalformedOutput = "The prover output is malformed" 1.58 + | string_of_atp_failure Interrupted = "The prover was interrupted" 1.59 + | string_of_atp_failure Crashed = "The prover crashed" 1.60 + | string_of_atp_failure InternalError = "An internal prover error occurred" 1.61 | string_of_atp_failure (UnknownError s) = 1.62 "A prover error occurred" ^ 1.63 - (if s = "" then ". (Pass the \"verbose\" option for details.)" 1.64 - else ":\n" ^ s) 1.65 + (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) 1.66 1.67 fun extract_delimited (begin_delim, end_delim) output = 1.68 (case first_field begin_delim output of