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