35 max_mono_iters : int option, |
35 max_mono_iters : int option, |
36 max_new_mono_instances : int option, |
36 max_new_mono_instances : int option, |
37 isar_proofs : bool option, |
37 isar_proofs : bool option, |
38 isar_compress : real, |
38 isar_compress : real, |
39 isar_try0 : bool, |
39 isar_try0 : bool, |
40 isar_minimize : bool, |
|
41 slice : bool, |
40 slice : bool, |
42 minimize : bool option, |
41 minimize : bool option, |
43 timeout : Time.time option, |
42 timeout : Time.time option, |
44 preplay_timeout : Time.time option, |
43 preplay_timeout : Time.time option, |
45 expect : string} |
44 expect : string} |
347 max_mono_iters : int option, |
346 max_mono_iters : int option, |
348 max_new_mono_instances : int option, |
347 max_new_mono_instances : int option, |
349 isar_proofs : bool option, |
348 isar_proofs : bool option, |
350 isar_compress : real, |
349 isar_compress : real, |
351 isar_try0 : bool, |
350 isar_try0 : bool, |
352 isar_minimize : bool, |
|
353 slice : bool, |
351 slice : bool, |
354 minimize : bool option, |
352 minimize : bool option, |
355 timeout : Time.time option, |
353 timeout : Time.time option, |
356 preplay_timeout : Time.time option, |
354 preplay_timeout : Time.time option, |
357 expect : string} |
355 expect : string} |
673 ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, |
671 ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, |
674 best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) |
672 best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) |
675 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
673 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
676 uncurried_aliases, fact_filter, max_facts, max_mono_iters, |
674 uncurried_aliases, fact_filter, max_facts, max_mono_iters, |
677 max_new_mono_instances, isar_proofs, isar_compress, |
675 max_new_mono_instances, isar_proofs, isar_compress, |
678 isar_try0, isar_minimize, slice, timeout, |
676 isar_try0, slice, timeout, preplay_timeout, ...}) |
679 preplay_timeout, ...}) |
|
680 minimize_command |
677 minimize_command |
681 ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = |
678 ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = |
682 let |
679 let |
683 val thy = Proof.theory_of state |
680 val thy = Proof.theory_of state |
684 val ctxt = Proof.context_of state |
681 val ctxt = Proof.context_of state |
950 Output.urgent_message "Generating proof text..." |
947 Output.urgent_message "Generating proof text..." |
951 else |
948 else |
952 () |
949 () |
953 val isar_params = |
950 val isar_params = |
954 (debug, verbose, preplay_timeout, isar_compress, isar_try0, |
951 (debug, verbose, preplay_timeout, isar_compress, isar_try0, |
955 isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, |
952 pool, fact_names, lifted, sym_tab, atp_proof, goal) |
956 goal) |
|
957 val one_line_params = |
953 val one_line_params = |
958 (preplay, proof_banner mode name, used_facts, |
954 (preplay, proof_banner mode name, used_facts, |
959 choose_minimize_command ctxt params minimize_command name |
955 choose_minimize_command ctxt params minimize_command name |
960 preplay, |
956 preplay, |
961 subgoal, subgoal_count) |
957 subgoal, subgoal_count) |