src/HOL/Tools/ATP/atp_proof.ML
changeset 41092 1b796ffa8347
parent 40684 c7ba327eb58c
child 41146 be78f4053bce
equal deleted inserted replaced
41091:0afdf5cde874 41092:1b796ffa8347
   107   | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
   107   | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
   108   | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
   108   | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
   109   | string_for_failure prover InternalError =
   109   | string_for_failure prover InternalError =
   110     "An internal " ^ prover ^ " error occurred."
   110     "An internal " ^ prover ^ " error occurred."
   111   | string_for_failure prover UnknownError =
   111   | string_for_failure prover UnknownError =
   112     "An unknown " ^ prover ^ " error occurred."
   112     (* "An" is correct for "ATP" and "SMT". *)
       
   113     "An " ^ prover ^ " error occurred."
   113 
   114 
   114 fun extract_delimited (begin_delim, end_delim) output =
   115 fun extract_delimited (begin_delim, end_delim) output =
   115   output |> first_field begin_delim |> the |> snd
   116   output |> first_field begin_delim |> the |> snd
   116          |> first_field end_delim |> the |> fst
   117          |> first_field end_delim |> the |> fst
   117          |> first_field "\n" |> the |> snd
   118          |> first_field "\n" |> the |> snd