| changeset 61560 | 7c985fd653c5 | 
| parent 61531 | ab2e862263e7 | 
| child 61649 | 268d88ec9087 | 
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Nov 03 16:35:38 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Nov 03 16:47:37 2015 +0100 @@ -6,7 +6,7 @@ section \<open>Multivariate calculus in Euclidean space\<close> theory Derivative -imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit" +imports Brouwer_Fixpoint Operator_Norm Uniform_Limit begin lemma netlimit_at_vector: (* TODO: move *)