
diff -r d08cb39b628a -r 6820684c7a58 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 31 10:24:29 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 31 10:42:31 2011 -0700
@@ -206,6 +206,9 @@
     by simp
 qed
 
+lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+  unfolding isCont_def by (rule tendsto_vec_nth)
+
 lemma eventually_Ball_finite: (* TODO: move *)
   assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
   shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
@@ -435,9 +438,6 @@
 apply (rule_tac x="1" in exI, simp add: norm_nth_le)
 done
 
-lemmas isCont_vec_nth [simp] =
-  bounded_linear.isCont [OF bounded_linear_vec_nth]
-
 instance vec :: (banach, finite) banach ..
 
 




