# HG changeset patch
# User desharna
# Date 1743773248 -7200
# Node ID ae2af2e085fdf5d25a26d0c7c991d9a807611dd6
# Parent  7230281bde03cab8ee92a0400aa8fc38284f4120
added proof method "iprover" to try0

diff -r 7230281bde03 -r ae2af2e085fd src/HOL/Tools/try0.ML
--- 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 =
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
 "]]