--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 12 22:41:25 2013 +0200
@@ -38,6 +38,8 @@
isar_compress : real,
isar_compress_degree : int,
merge_timeout_slack : real,
+ isar_try0 : bool,
+ isar_minimize : bool,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -351,6 +353,8 @@
isar_compress : real,
isar_compress_degree : int,
merge_timeout_slack : real,
+ isar_try0 : bool,
+ isar_minimize : bool,
slice : bool,
minimize : bool option,
timeout : Time.time option,
@@ -684,6 +688,7 @@
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_compress,
isar_compress_degree, merge_timeout_slack,
+ isar_try0, isar_minimize,
slice, timeout, preplay_timeout, preplay_trace, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
@@ -959,6 +964,7 @@
val isar_params =
(debug, verbose, preplay_timeout, preplay_trace, isar_compress,
isar_compress_degree, merge_timeout_slack,
+ isar_try0,isar_minimize,
pool, fact_names, lifted, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,