author | wenzelm |
Wed, 03 Nov 2021 11:51:42 +0100 | |
changeset 74667 | 0b3dc8c5fb32 |
parent 74666 | 432b3605933d |
child 74669 | 74f044c3e590 |
child 74670 | b2604cd4d131 |
--- 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