# HG changeset patch
# User paulson
# Date 1744135569 -3600
# Node ID 67c024ec618e92179bc864f848653efa422915e6
# Parent  c7bd567723b141cfd1b62689b3a1abb1118fae69# Parent  a1de627d417ae66a0d05fa64e0e65df7de49441c
merged

diff -r a1de627d417a -r 67c024ec618e src/HOL/Try0_HOL.thy
--- a/src/HOL/Try0_HOL.thy	Tue Apr 08 19:06:00 2025 +0100
+++ b/src/HOL/Try0_HOL.thy	Tue Apr 08 19:06:09 2025 +0100
@@ -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
 "]]