# HG changeset patch
# User immler
# Date 1366648752 -7200
# Node ID 70abecafe9ac6ca8b9c87c0a8e8c5c724695222c
# Parent  4392eb046a975141734415bff90135399223c401
removed type constraints

diff -r 4392eb046a97 -r 70abecafe9ac src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 22 16:36:02 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Apr 22 18:39:12 2013 +0200
@@ -1433,7 +1433,6 @@
 qed
 
 lemma vector_derivative_unique_within_closed_interval:
-  fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
   assumes "a < b" and "x \<in> {a..b}"
   assumes "(f has_vector_derivative f') (at x within {a..b})"
   assumes "(f has_vector_derivative f'') (at x within {a..b})"
@@ -1460,7 +1459,6 @@
   unfolding has_vector_derivative_def by auto
 
 lemma vector_derivative_within_closed_interval:
-  fixes f::"real \<Rightarrow> 'a::ordered_euclidean_space"
   assumes "a < b" and "x \<in> {a..b}"
   assumes "(f has_vector_derivative f') (at x within {a..b})"
   shows "vector_derivative f (at x within {a..b}) = f'"