author | wenzelm |
Tue, 09 Nov 2021 17:20:04 +0100 | |
changeset 74739 | a06652d397a7 |
parent 74738 | cba1da393958 |
child 74740 | d14918fcbd37 |
--- 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