# HG changeset patch
# User huffman
# Date 1314316255 25200
# Node ID adb18b07b34113b28dfb7ac82ee3dfaf104be36e
# Parent  d4d9ea33703c0c2bede9ac9cf1472084b0f92b69
remove legacy theorem Lim_inner

diff -r d4d9ea33703c -r adb18b07b341 NEWS
--- a/NEWS	Thu Aug 25 16:42:13 2011 -0700
+++ b/NEWS	Thu Aug 25 16:50:55 2011 -0700
@@ -218,6 +218,7 @@
   Lim_linear ~> bounded_linear.tendsto
   Lim_component ~> tendsto_euclidean_component
   Lim_component_cart ~> tendsto_vec_nth
+  Lim_inner ~> tendsto_inner [OF tendsto_const]
   dot_lsum ~> inner_setsum_left
   dot_rsum ~> inner_setsum_right
   subset_interior ~> interior_mono
diff -r d4d9ea33703c -r adb18b07b341 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 16:42:13 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 16:50:55 2011 -0700
@@ -5104,10 +5104,6 @@
   finally show ?thesis .
 qed
 
-lemma Lim_inner:
-  assumes "(f ---> l) net"  shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
-  by (intro tendsto_intros assms)
-
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)