--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -379,10 +379,9 @@
(override_params prover type_enc (my_timeout time_slice)) fact_override []
in
if meth = "sledgehammer_tac" then
- sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
- ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
+ sledge_tac 0.25 ATP_Proof.vampireN "mono_native"
+ ORELSE' sledge_tac 0.25 ATP_Proof.eN "poly_guards??"
+ ORELSE' sledge_tac 0.25 ATP_Proof.spassN "mono_native"
ORELSE' SMT_Solver.smt_tac ctxt thms
else if meth = "smt" then
SMT_Solver.smt_tac ctxt thms