--- a/src/HOL/Tools/try0.ML Wed Apr 02 11:18:35 2025 +0200
+++ b/src/HOL/Tools/try0.ML Fri Apr 04 15:27:28 2025 +0200
@@ -107,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 =
--- 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
"]]