--- 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 =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Sep 25 17:16:32 2023 +0200
@@ -18,6 +18,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -60,6 +61,7 @@
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
+ Argo_Method |
Blast_Method |
Simp_Method |
Auto_Method |
@@ -101,6 +103,7 @@
| SMT_Method (SMT_Verit strategy) =>
"smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
| SATx_Method => "satx"
+ | Argo_Method => "argo"
| Blast_Method => "blast"
| Simp_Method => if null ss then "simp" else "simp add:"
| Auto_Method => "auto"
@@ -141,6 +144,7 @@
Method.insert_tac ctxt global_facts THEN'
(case meth of
SATx_Method => SAT.satx_tac ctxt
+ | Argo_Method => Argo_Tactic.argo_tac ctxt []
| Blast_Method => blast_tac ctxt
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Sep 25 17:16:32 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Sep 25 17:16:32 2023 +0200
@@ -217,7 +217,8 @@
let
val misc_methodss =
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
- Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]]
+ Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
+ Argo_Method]]
val metis_methodss =
[Metis_Method (SOME full_typesN, NONE) ::