# HG changeset patch # User desharna # Date 1639865828 -3600 # Node ID 74c53a9027e291d11387a6ce4802eb24b35a9ea3 # Parent aade20a03edb817fa9dc127f99efa6e681c21aaf used TH1 for Leo-III in sledgehammer diff -r aade20a03edb -r 74c53a9027e2 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Dec 18 23:11:49 2021 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Dec 18 23:17:08 2021 +0100 @@ -384,7 +384,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((512, ""), TH1, "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances}