# HG changeset patch
# User himmelma
# Date 1265029932 -3600
# Node ID 475aef44d5fb4814dff7fd2f606a0279d7d86f87
# Parent  6676fd863e02727bf4702b43971a78f94f771c99
Removed explicit type annotations

diff -r 6676fd863e02 -r 475aef44d5fb src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Jan 31 19:07:03 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Feb 01 14:12:12 2010 +0100
@@ -1252,22 +1252,21 @@
   using vector_derivative_works[unfolded differentiable_def]
   using assms by(auto simp add:has_vector_derivative_def)
 
-lemma has_vector_derivative_within_subset: fixes f::"real \<Rightarrow> real^'a" shows
+lemma has_vector_derivative_within_subset: 
  "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
   unfolding has_vector_derivative_def apply(rule has_derivative_within_subset) by auto
 
-lemma has_vector_derivative_const: fixes c::"real^'n" shows
+lemma has_vector_derivative_const: 
  "((\<lambda>x. c) has_vector_derivative 0) net"
   unfolding has_vector_derivative_def using has_derivative_const by auto
 
 lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
   unfolding has_vector_derivative_def using has_derivative_id by auto
 
-lemma has_vector_derivative_cmul: fixes f::"real \<Rightarrow> real^'a"
-  shows "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
+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"
   unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps)
 
-lemma has_vector_derivative_cmul_eq: fixes f::"real \<Rightarrow> real^'a" assumes "c \<noteq> 0"
+lemma has_vector_derivative_cmul_eq: assumes "c \<noteq> 0"
   shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
   apply rule apply(drule has_vector_derivative_cmul[where c="1/c"]) defer
   apply(rule has_vector_derivative_cmul) using assms by auto