--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 15:56:48 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 16:35:50 2011 -0700
@@ -1526,9 +1526,9 @@
lemma has_derivative_vmul_component_cart: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
assumes "(c has_derivative c') net"
- shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net"
- using has_derivative_vmul_component[OF assms]
- unfolding nth_conv_component .
+ shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net"
+ unfolding nth_conv_component
+ by (intro has_derivative_intros assms)
lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
@@ -1641,8 +1641,6 @@
lemma vec1_component[simp]: "(vec1 x)$1 = x"
by (simp_all add: vec_eq_iff)
-declare vec1_dest_vec1(1) [simp]
-
lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
by (metis vec1_dest_vec1(1))