1.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Jan 31 19:07:03 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Feb 01 14:12:12 2010 +0100
     1.3 @@ -1252,22 +1252,21 @@
     1.4    using vector_derivative_works[unfolded differentiable_def]
     1.5    using assms by(auto simp add:has_vector_derivative_def)
     1.6  
     1.7 -lemma has_vector_derivative_within_subset: fixes f::"real \<Rightarrow> real^'a" shows
     1.8 +lemma has_vector_derivative_within_subset: 
     1.9   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
    1.10    unfolding has_vector_derivative_def apply(rule has_derivative_within_subset) by auto
    1.11  
    1.12 -lemma has_vector_derivative_const: fixes c::"real^'n" shows
    1.13 +lemma has_vector_derivative_const: 
    1.14   "((\<lambda>x. c) has_vector_derivative 0) net"
    1.15    unfolding has_vector_derivative_def using has_derivative_const by auto
    1.16  
    1.17  lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
    1.18    unfolding has_vector_derivative_def using has_derivative_id by auto
    1.19  
    1.20 -lemma has_vector_derivative_cmul: fixes f::"real \<Rightarrow> real^'a"
    1.21 -  shows "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
    1.22 +lemma has_vector_derivative_cmul:  "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
    1.23    unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps)
    1.24  
    1.25 -lemma has_vector_derivative_cmul_eq: fixes f::"real \<Rightarrow> real^'a" assumes "c \<noteq> 0"
    1.26 +lemma has_vector_derivative_cmul_eq: assumes "c \<noteq> 0"
    1.27    shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
    1.28    apply rule apply(drule has_vector_derivative_cmul[where c="1/c"]) defer
    1.29    apply(rule has_vector_derivative_cmul) using assms by auto