equal
deleted
inserted
replaced
47 {comment : string, |
47 {comment : string, |
48 state : Proof.state, |
48 state : Proof.state, |
49 goal : thm, |
49 goal : thm, |
50 subgoal : int, |
50 subgoal : int, |
51 subgoal_count : int, |
51 subgoal_count : int, |
52 factss : (string * fact list) list} |
52 factss : (string * fact list) list, |
|
53 found_proof : unit -> unit} |
53 |
54 |
54 type prover_result = |
55 type prover_result = |
55 {outcome : atp_failure option, |
56 {outcome : atp_failure option, |
56 used_facts : (string * stature) list, |
57 used_facts : (string * stature) list, |
57 used_from : fact list, |
58 used_from : fact list, |
131 {comment : string, |
132 {comment : string, |
132 state : Proof.state, |
133 state : Proof.state, |
133 goal : thm, |
134 goal : thm, |
134 subgoal : int, |
135 subgoal : int, |
135 subgoal_count : int, |
136 subgoal_count : int, |
136 factss : (string * fact list) list} |
137 factss : (string * fact list) list, |
|
138 found_proof : unit -> unit} |
137 |
139 |
138 type prover_result = |
140 type prover_result = |
139 {outcome : atp_failure option, |
141 {outcome : atp_failure option, |
140 used_facts : (string * stature) list, |
142 used_facts : (string * stature) list, |
141 used_from : fact list, |
143 used_from : fact list, |