removed iprover from try0 because its name is clashing with iProver in Sledgehammer
--- a/src/HOL/Try0_HOL.thy Mon Apr 07 12:36:56 2025 +0200
+++ b/src/HOL/Try0_HOL.thy Tue Apr 08 17:36:07 2025 +0200
@@ -43,7 +43,6 @@
("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
@@ -64,7 +63,7 @@
\<close>
declare [[try0_schedule = "
- satx iprover metis |
+ satx metis |
order presburger linarith algebra argo |
simp auto blast fast fastforce force meson
"]]