--- a/src/HOL/Analysis/Analysis.thy Wed Aug 28 00:08:14 2019 +0200
+++ b/src/HOL/Analysis/Analysis.thy Wed Aug 28 08:51:20 2019 +0200
@@ -43,7 +43,7 @@
Generalised_Binomial_Theorem
Gamma_Function
Change_Of_Vars
- Lipschitz
+ Multivariate_Analysis
Simplex_Content
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Multivariate_Analysis.thy Wed Aug 28 08:51:20 2019 +0200
@@ -0,0 +1,12 @@
+theory
+ Multivariate_Analysis
+imports
+ Ordered_Euclidean_Space
+ Determinants
+ Cross3
+ Lipschitz
+begin
+
+text \<open>Entry point excluding integration and complex analysis.\<close>
+
+end
\ No newline at end of file