diff -r 7230281bde03 -r ae2af2e085fd src/HOL/Try0_HOL.thy
--- a/src/HOL/Try0_HOL.thy	Wed Apr 02 11:18:35 2025 +0200
+++ b/src/HOL/Try0_HOL.thy	Fri Apr 04 15:27:28 2025 +0200
@@ -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
@@ -63,7 +64,7 @@
 \<close>
 
 declare [[try0_schedule = "
-  satx metis |
+  satx iprover metis |
   order presburger linarith algebra argo |
   simp auto blast fast fastforce force meson
 "]]