--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 25 17:16:32 2023 +0200
@@ -134,9 +134,12 @@
bool * (string option * string option) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
-val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
-val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
+val basic_systematic_methods =
+ [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method, Argo_Method]
+val basic_simp_based_methods =
+ [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
+val basic_arith_methods =
+ [Linarith_Method, Presburger_Method, Algebra_Method]
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
val systematic_methods =