removed iprover from try0 because its name is clashing with iProver in Sledgehammer
authordesharna
Tue, 08 Apr 2025 17:36:07 +0200
changeset 82458 c7bd567723b1
parent 82457 5a0d1075911c
child 82460 67c024ec618e
removed iprover from try0 because its name is clashing with iProver in Sledgehammer
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
 "]]