equal
deleted
inserted
replaced
36 OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError |
36 OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError |
37 type prover_result = |
37 type prover_result = |
38 {outcome: failure option, |
38 {outcome: failure option, |
39 message: string, |
39 message: string, |
40 pool: string Symtab.table, |
40 pool: string Symtab.table, |
41 relevant_thm_names: string list, |
41 used_thm_names: string list, |
42 atp_run_time_in_msecs: int, |
42 atp_run_time_in_msecs: int, |
43 output: string, |
43 output: string, |
44 proof: string, |
44 proof: string, |
45 internal_thm_names: string Vector.vector, |
45 internal_thm_names: string Vector.vector, |
46 conjecture_shape: int list, |
46 conjecture_shape: int list, |
105 |
105 |
106 type prover_result = |
106 type prover_result = |
107 {outcome: failure option, |
107 {outcome: failure option, |
108 message: string, |
108 message: string, |
109 pool: string Symtab.table, |
109 pool: string Symtab.table, |
110 relevant_thm_names: string list, |
110 used_thm_names: string list, |
111 atp_run_time_in_msecs: int, |
111 atp_run_time_in_msecs: int, |
112 output: string, |
112 output: string, |
113 proof: string, |
113 proof: string, |
114 internal_thm_names: string Vector.vector, |
114 internal_thm_names: string Vector.vector, |
115 conjecture_shape: int list, |
115 conjecture_shape: int list, |