--- 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
--- 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>
--- 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