| changeset 74667 | 0b3dc8c5fb32 |
| parent 70956 | 860198428664 |
| child 74736 | df4449c6eff1 |
--- a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Wed Nov 03 11:02:36 2021 +0100 +++ b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Wed Nov 03 11:51:42 2021 +0100 @@ -54,7 +54,7 @@ by metric lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e" - by metric + using [[argo_timeout = 25]] by metric lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y" by metric