merged

--- a/NEWS	Fri Apr 04 16:37:58 2025 +0100
+++ b/NEWS	Fri Apr 04 16:38:16 2025 +0100
@@ -35,15 +35,15 @@
 
 * Theory "HOL.Fun":
   - Added lemmas.
-      mono_on_strict_invE
-      mono_on_invE
-      strict_mono_on_eq
-      strict_mono_on_less_eq
-      strict_mono_on_less
       antimonotone_on_inf_fun
       antimonotone_on_sup_fun
+      mono_on_invE
+      mono_on_strict_invE
       monotone_on_inf_fun
       monotone_on_sup_fun
+      strict_mono_on_eq
+      strict_mono_on_less
+      strict_mono_on_less_eq
   - Removed lemmas. Minor INCOMPATIBILITY.
       mono_on_greaterD (use mono_invE instead)
 

--- a/src/HOL/Sledgehammer.thy	Fri Apr 04 16:37:58 2025 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Apr 04 16:38:16 2025 +0100
@@ -7,7 +7,15 @@
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
-imports Presburger SMT Try0_HOL
+  imports
+    \<comment> \<open>FIXME: \<^theory>\<open>HOL.Try0_HOL\<close> has to be imported first so that @{attribute try0_schedule} gets
+    the value assigned value there. Otherwise, the value is the one assigned in \<^theory>\<open>HOL.Try0\<close>,
+    which is imported transitively by both \<^theory>\<open>HOL.Presburger\<close> and \<^theory>\<open>HOL.SMT\<close>. It seems
+    that, when merging the attributes from two theories, the value assigned int the leftmost theory
+    has precedence.\<close>
+    Try0_HOL
+    Presburger
+    SMT
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl

--- a/src/HOL/Tools/try0.ML	Fri Apr 04 16:37:58 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Apr 04 16:38:16 2025 +0100
@@ -29,6 +29,8 @@
   val get_proof_method_or_noop : string -> proof_method
   val get_all_proof_method_names : unit -> string list
 
+  val schedule : string Config.T
+
   datatype mode = Auto_Try | Try | Normal
   val generic_try0 : mode -> Time.time option -> facts -> Proof.state ->
     (bool * (string * string list)) * result list
@@ -95,15 +97,9 @@
 fun get_proof_method (name : string) : proof_method option =
   Symtab.lookup (Synchronized.value proof_methods) name;
 
-fun get_all_proof_methods () : (string * proof_method) list =
-  Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) []
-
 fun get_all_proof_method_names () : string list =
   Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) []
 
-fun get_all_auto_try_proof_method_names () : string list =
-  Symset.dest (Synchronized.value auto_try_proof_methods_names)
-
 fun should_auto_try_proof_method (name : string) : bool =
   Symset.member (Synchronized.value auto_try_proof_methods_names) name
 
@@ -111,7 +107,7 @@
 
 fun get_proof_method_or_noop name =
   (case get_proof_method name of
-    NONE => noop_proof_method
+    NONE => (warning ("Proof method \"" ^ name ^ "\" is undefined"); noop_proof_method)
   | SOME proof_method => proof_method)
 
 fun maybe_apply_proof_method name mode : proof_method =
@@ -120,10 +116,15 @@
   else
     noop_proof_method
 
+val schedule = Attrib.setup_config_string \<^binding>\<open>try0_schedule\<close> (K "")
+
+local
+
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
 
-fun generic_try0 mode timeout_opt (facts : facts) st =
+fun generic_try0_step mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state)
+  (proof_methods : string list) =
   let
     fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st
     fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
@@ -139,11 +140,10 @@
         methods
         |> Par_List.get_some try_method
         |> the_list
-    val proof_method_names = get_all_proof_method_names ()
-    val maybe_apply_methods = map maybe_apply_proof_method proof_method_names
+    val maybe_apply_methods = map maybe_apply_proof_method proof_methods
   in
     if mode = Normal then
-      let val names = map quote proof_method_names in
+      let val names = map quote proof_methods in
         writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...")
       end
     else
@@ -171,6 +171,31 @@
       end)
   end
 
+in
+
+fun generic_try0 mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state) =
+  let
+    fun some_nonempty_string sub =
+      if Substring.isEmpty sub then
+        NONE
+      else
+        SOME (Substring.string sub)
+    val schedule =
+      Config.get (Proof.context_of st) schedule
+      |> Substring.full
+      |> Substring.tokens (fn c => c = #"|")
+      |> map (map_filter some_nonempty_string o Substring.tokens Char.isSpace)
+    fun iterate [] = ((false, (noneN, [])), [])
+      | iterate (proof_methods :: proof_methodss) =
+        (case generic_try0_step mode timeout_opt facts st proof_methods of
+          (_, []) => iterate proof_methodss
+        | result as (_, _ :: _) => result)
+  in
+    iterate (if null schedule then [get_all_proof_method_names ()] else schedule)
+  end;
+
+end
+
 fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt
 
 fun try0_trans (facts : facts) =

--- a/src/HOL/Try0_HOL.thy	Fri Apr 04 16:37:58 2025 +0100
+++ b/src/HOL/Try0_HOL.thy	Fri Apr 04 16:38:16 2025 +0100
@@ -43,6 +43,7 @@
    ("force", (false, (false, full_attrs))),
    ("meson", (false, (false, metis_attrs))),
    ("satx", (false, (false, no_attrs))),
+   ("iprover", (false, (false, no_attrs))),
    ("order", (true, (false, no_attrs)))]
 
 in
@@ -62,4 +63,10 @@
 end
 \<close>
 
+declare [[try0_schedule = "
+  satx iprover metis |
+  order presburger linarith algebra argo |
+  simp auto blast fast fastforce force meson
+"]]
+
 end
\ No newline at end of file