equal
deleted
inserted
replaced
61 subgoal : int, |
61 subgoal : int, |
62 subgoal_count : int, |
62 subgoal_count : int, |
63 factss : (string * fact list) list, |
63 factss : (string * fact list) list, |
64 found_proof : string -> unit} |
64 found_proof : string -> unit} |
65 |
65 |
66 type prover_slice = base_slice * atp_slice option |
66 datatype prover_slice_extra = |
|
67 ATP_Slice of atp_slice |
|
68 | SMT_Slice of string list |
|
69 |
|
70 type prover_slice = base_slice * prover_slice_extra |
67 |
71 |
68 type prover_result = |
72 type prover_result = |
69 {outcome : atp_failure option, |
73 {outcome : atp_failure option, |
70 used_facts : (string * stature) list, |
74 used_facts : (string * stature) list, |
71 used_from : fact list, |
75 used_from : fact list, |
174 subgoal : int, |
178 subgoal : int, |
175 subgoal_count : int, |
179 subgoal_count : int, |
176 factss : (string * fact list) list, |
180 factss : (string * fact list) list, |
177 found_proof : string -> unit} |
181 found_proof : string -> unit} |
178 |
182 |
179 type prover_slice = base_slice * atp_slice option |
183 datatype prover_slice_extra = |
|
184 ATP_Slice of atp_slice |
|
185 | SMT_Slice of string list |
|
186 |
|
187 type prover_slice = base_slice * prover_slice_extra |
180 |
188 |
181 type prover_result = |
189 type prover_result = |
182 {outcome : atp_failure option, |
190 {outcome : atp_failure option, |
183 used_facts : (string * stature) list, |
191 used_facts : (string * stature) list, |
184 used_from : fact list, |
192 used_from : fact list, |