# HG changeset patch
# User nipkow
# Date 1516259316 -3600
# Node ID afefc45ed4e957722355241e209c2e309f5e5b18
# Parent  aab817885622fe31ae45bac0a18aba82823705a7
more automation

diff -r aab817885622 -r afefc45ed4e9 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Jan 17 12:27:06 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Jan 18 08:08:36 2018 +0100
@@ -760,7 +760,7 @@
     and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
   using assms by (auto simp: order_tendsto_iff)
 
-lemma (in linorder_topology) tendsto_max:
+lemma (in linorder_topology) tendsto_max[tendsto_intros]:
   assumes X: "(X \<longlongrightarrow> x) net"
     and Y: "(Y \<longlongrightarrow> y) net"
   shows "((\<lambda>x. max (X x) (Y x)) \<longlongrightarrow> max x y) net"
@@ -778,7 +778,7 @@
     by (auto simp: eventually_conj_iff)
 qed
 
-lemma (in linorder_topology) tendsto_min:
+lemma (in linorder_topology) tendsto_min[tendsto_intros]:
   assumes X: "(X \<longlongrightarrow> x) net"
     and Y: "(Y \<longlongrightarrow> y) net"
   shows "((\<lambda>x. min (X x) (Y x)) \<longlongrightarrow> min x y) net"