--- 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
"]]