equal
deleted
inserted
replaced
56 {outcome : atp_failure option, |
56 {outcome : atp_failure option, |
57 used_facts : (string * stature) list, |
57 used_facts : (string * stature) list, |
58 used_from : fact list, |
58 used_from : fact list, |
59 preferred_methss : proof_method * proof_method list list, |
59 preferred_methss : proof_method * proof_method list list, |
60 run_time : Time.time, |
60 run_time : Time.time, |
61 message : proof_method * play_outcome -> string, |
61 message : proof_method * play_outcome -> string} |
62 message_tail : string} |
|
63 |
62 |
64 type prover = params -> prover_problem -> prover_result |
63 type prover = params -> prover_problem -> prover_result |
65 |
64 |
66 val SledgehammerN : string |
65 val SledgehammerN : string |
67 val str_of_mode : mode -> string |
66 val str_of_mode : mode -> string |
148 {outcome : atp_failure option, |
147 {outcome : atp_failure option, |
149 used_facts : (string * stature) list, |
148 used_facts : (string * stature) list, |
150 used_from : fact list, |
149 used_from : fact list, |
151 preferred_methss : proof_method * proof_method list list, |
150 preferred_methss : proof_method * proof_method list list, |
152 run_time : Time.time, |
151 run_time : Time.time, |
153 message : proof_method * play_outcome -> string, |
152 message : proof_method * play_outcome -> string} |
154 message_tail : string} |
|
155 |
153 |
156 type prover = params -> prover_problem -> prover_result |
154 type prover = params -> prover_problem -> prover_result |
157 |
155 |
158 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) |
156 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) |
159 |
157 |