# HG changeset patch
# User boehmes
# Date 1475175285 -7200
# Node ID 2fd9656c4c827c33b3839043ebefda4361c14f93
# Parent  3daf02070be5f54e28bcfd9fba7e4f29c575b173
invoke argo as part of the tried automatic proof methods

diff -r 3daf02070be5 -r 2fd9656c4c82 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Sep 29 20:54:44 2016 +0200
+++ b/src/HOL/Presburger.thy	Thu Sep 29 20:54:45 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Decision Procedure for Presburger Arithmetic\<close>
 
 theory Presburger
-imports Groebner_Basis Set_Interval
+imports Groebner_Basis Set_Interval Argo
 keywords "try0" :: diag
 begin
 
diff -r 3daf02070be5 -r 2fd9656c4c82 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Sep 29 20:54:44 2016 +0200
+++ b/src/HOL/Real.thy	Thu Sep 29 20:54:45 2016 +0200
@@ -10,7 +10,7 @@
 section \<open>Development of the Reals using Cauchy Sequences\<close>
 
 theory Real
-imports Rat Argo
+imports Rat
 begin
 
 text \<open>
diff -r 3daf02070be5 -r 2fd9656c4c82 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Sep 29 20:54:44 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Sep 29 20:54:45 2016 +0200
@@ -88,6 +88,7 @@
    ("auto", ((true, true), full_attrs)),
    ("blast", ((false, true), clas_attrs)),
    ("metis", ((false, true), metis_attrs)),
+   ("argo", ((false, true), no_attrs)),
    ("linarith", ((false, true), no_attrs)),
    ("presburger", ((false, true), no_attrs)),
    ("algebra", ((false, true), no_attrs)),
@@ -111,6 +112,7 @@
       |> Simplifier_Trace.disable
       |> Context_Position.set_visible false
       |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound)
+      |> Config.put Argo_Tactic.trace "none"
       |> Proof_Context.background_theory (fn thy =>
           thy
           |> Context_Position.set_visible_global false