# HG changeset patch
# User wenzelm
# Date 1636474804 -3600
# Node ID a06652d397a7f811b50721545b27383811b959f3
# Parent  cba1da393958ac15a155abaadf5d3472705d83ff
more robust timeout, following df4449c6eff1;

diff -r cba1da393958 -r a06652d397a7 src/HOL/Eisbach/Example_Metric.thy
--- a/src/HOL/Eisbach/Example_Metric.thy	Tue Nov 09 11:23:27 2021 +0100
+++ b/src/HOL/Eisbach/Example_Metric.thy	Tue Nov 09 17:20:04 2021 +0100
@@ -8,6 +8,8 @@
 text \<open>An Eisbach implementation of the method @{method metric}.
   Slower than the Isabelle/ML implementation but arguably more readable.\<close>
 
+declare [[argo_timeout = 20]]
+
 method dist_refl_sym = simp only: simp_thms dist_commute dist_self
 
 method lin_real_arith uses thms = argo thms