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