# HG changeset patch
# User huffman
# Date 1395353635 25200
# Node ID 67a5f004583da890fb2136e64981e9b2cb5573b2
# Parent  29fd6bd9228e7cf554db6adcce0200f7d9bbec25
generalize more theorems

diff -r 29fd6bd9228e -r 67a5f004583d src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 09:21:39 2014 -0700
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Mar 20 15:13:55 2014 -0700
@@ -888,7 +888,7 @@
 text {* In particular. *}
 
 lemma has_derivative_zero_constant:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   assumes "convex s"
     and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
   shows "\<exists>c. \<forall>x\<in>s. f x = c"
@@ -914,7 +914,7 @@
 qed
 
 lemma has_derivative_zero_unique:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
   assumes "convex s"
     and "a \<in> s"
     and "f a = c"
@@ -1184,7 +1184,7 @@
 text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}
 
 lemma sussmann_open_mapping:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
   assumes "open s"
     and "continuous_on s f"
     and "x \<in> s"