equal
deleted
inserted
replaced
33 axiom_clauses: (thm * (string * int)) list option, |
33 axiom_clauses: (thm * (string * int)) list option, |
34 filtered_clauses: (thm * (string * int)) list option} |
34 filtered_clauses: (thm * (string * int)) list option} |
35 type prover_result = |
35 type prover_result = |
36 {success: bool, |
36 {success: bool, |
37 message: string, |
37 message: string, |
38 conjecture_pos: int * int, |
|
39 relevant_thm_names: string list, |
38 relevant_thm_names: string list, |
40 atp_run_time_in_msecs: int, |
39 atp_run_time_in_msecs: int, |
41 proof: string, |
40 proof: string, |
42 internal_thm_names: string Vector.vector, |
41 internal_thm_names: string Vector.vector, |
43 filtered_clauses: (thm * (string * int)) list} |
42 filtered_clauses: (thm * (string * int)) list} |
90 filtered_clauses: (thm * (string * int)) list option}; |
89 filtered_clauses: (thm * (string * int)) list option}; |
91 |
90 |
92 type prover_result = |
91 type prover_result = |
93 {success: bool, |
92 {success: bool, |
94 message: string, |
93 message: string, |
95 conjecture_pos: int * int, |
|
96 relevant_thm_names: string list, |
94 relevant_thm_names: string list, |
97 atp_run_time_in_msecs: int, |
95 atp_run_time_in_msecs: int, |
98 proof: string, |
96 proof: string, |
99 internal_thm_names: string Vector.vector, |
97 internal_thm_names: string Vector.vector, |
100 filtered_clauses: (thm * (string * int)) list}; |
98 filtered_clauses: (thm * (string * int)) list}; |