# HG changeset patch
# User desharna
# Date 1744126567 -7200
# Node ID c7bd567723b141cfd1b62689b3a1abb1118fae69
# Parent  5a0d1075911cdf330a0a47af37cac09c16c27df3
removed iprover from try0 because its name is clashing with iProver in Sledgehammer

diff -r 5a0d1075911c -r c7bd567723b1 src/HOL/Try0_HOL.thy
--- 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
 "]]