changeset 58877 | 262572d90bc6 |
parent 57865 | dcfb33c26f50 |
child 59558 | 5d9f0ace9af0 |
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Nov 02 17:06:05 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Nov 02 17:09:04 2014 +0100 @@ -3,7 +3,7 @@ Author: Robert Himmelmann, TU Muenchen (translation from HOL Light) *) -header {* Multivariate calculus in Euclidean space *} +section {* Multivariate calculus in Euclidean space *} theory Derivative imports Brouwer_Fixpoint Operator_Norm