# HG changeset patch
# User huffman
# Date 1312965413 25200
# Node ID 5fc334b94e0057c51a1486b0d1a14a6140387ed1
# Parent  f046f5794f2ad7b4072d0165fd6720988ef929dc
declare tendsto_const [intro] (accidentally removed in 230a8665c919)

diff -r f046f5794f2a -r 5fc334b94e00 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 00:31:51 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 01:36:53 2011 -0700
@@ -6098,6 +6098,8 @@
 (** TODO move this someplace else within this theory **)
 instance euclidean_space \<subseteq> banach ..
 
+declare tendsto_const [intro] (* FIXME: move *)
+
 text {* Legacy theorem names *}
 
 lemmas Lim_ident_at = LIM_ident