--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jan 31 16:09:23 2022 +0100
@@ -63,6 +63,7 @@
("fact_thresholds", "0.45 0.85"),
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
+ ("max_proofs", "4"),
("isar_proofs", "smart"),
("compress", "smart"),
("try0", "true"),
@@ -259,6 +260,7 @@
val max_mono_iters = lookup_option lookup_int "max_mono_iters"
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
+ val max_proofs = lookup_int "max_proofs"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
val try0 = lookup_bool "try0"
@@ -274,9 +276,9 @@
uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
- isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
- minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0,
+ smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params