more generous timeout: support build on Raspberry Pi;
authorwenzelm
Wed, 03 Nov 2021 11:51:42 +0100
changeset 74667 0b3dc8c5fb32
parent 74666 432b3605933d
child 74669 74f044c3e590
child 74670 b2604cd4d131
more generous timeout: support build on Raspberry Pi;
src/HOL/Analysis/ex/Metric_Arith_Examples.thy
--- 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