656 val dummy_thf_format = THF (Polymorphic, THF_With_Choice) |
656 val dummy_thf_format = THF (Polymorphic, THF_With_Choice) |
657 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false |
657 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false |
658 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) |
658 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) |
659 |
659 |
660 val spass_pirate_format = DFG Polymorphic |
660 val spass_pirate_format = DFG Polymorphic |
661 val remote_spass_pirate_config = |
661 val remote_spass_pirate_config : atp_config = |
662 {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]), |
662 {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]), |
663 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
663 arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ => |
664 string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
664 string_of_int (to_secs 1 timeout) ^ " " ^ file_name, |
665 proof_delims = [("Involved clauses:", "Involved clauses:")], |
665 proof_delims = [("Involved clauses:", "Involved clauses:")], |
666 known_failures = known_szs_status_failures, |
666 known_failures = known_szs_status_failures, |