src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Oct 24 22:05:57 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Oct 25 15:31:58 2024 +0200
@@ -71,6 +71,7 @@
    ("compress", "smart"),
    ("try0", "true"),
    ("smt_proofs", "true"),
+   ("suggest_of", "smart"),
    ("minimize", "true"),
    ("slices", string_of_int (12 * Multithreading.max_threads ())),
    ("preplay_timeout", "1")]
@@ -94,7 +95,8 @@
    ("no_isar_proofs", "isar_proofs"),
    ("dont_minimize", "minimize"),
    ("dont_try0", "try0"),
-   ("no_smt_proofs", "smt_proofs")]
+   ("no_smt_proofs", "smt_proofs"),
+   ("dont_suggest_of", "suggest_of")]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -264,6 +266,7 @@
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_bool "smt_proofs"
+    val suggest_of = lookup_option lookup_bool "suggest_of"
     val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
     val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices")
     val timeout = lookup_time "timeout"
@@ -277,8 +280,8 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, 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}
+     suggest_of = suggest_of, minimize = minimize, slices = slices, timeout = timeout,
+     preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params