# HG changeset patch
# User wenzelm
# Date 1635936702 -3600
# Node ID 0b3dc8c5fb326a5ffe8569aa2468e00ab9e5c0a4
# Parent  432b3605933d055ddff0011882fadc195e052bcc
more generous timeout: support build on Raspberry Pi;

diff -r 432b3605933d -r 0b3dc8c5fb32 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