Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
declare tendsto_const [intro] (accidentally removed in 230a8665c919)
authorhuffman
Wed, 10 Aug 2011 01:36:53 -0700
changeset 44131 5fc334b94e00
parent 44130 f046f5794f2a
child 44132 0f35a870ecf1
declare tendsto_const [intro] (accidentally removed in 230a8665c919)
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle