src/HOL/Tools/ATP/atp_proof.ML

     if output = "" then "No details available" else elide_string 1000 output
   else
     ""
 
 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
     SOME (_, tail) =>
     (case first_field "\n" tail of