# HG changeset patch
# User blanchet
# Date 1695654992 -7200
# Node ID 41273636a82a653133191839dad49ad4c7e59da1
# Parent  5e995ceb7490b228ca4e577b69d9e414ab6aacfe
added argo

diff -r 5e995ceb7490 -r 41273636a82a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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 =
diff -r 5e995ceb7490 -r 41273636a82a src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- 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
diff -r 5e995ceb7490 -r 41273636a82a src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- 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) ::