# HG changeset patch
# User immler
# Date 1566975080 -7200
# Node ID 1afcfb7fdff41a9b0d1def6e6d3e6f761ea1cbdf
# Parent  f95193669ad7e0feefd5ea4fc43ea36c666277c5
entry point for analysis without integration theory

diff -r f95193669ad7 -r 1afcfb7fdff4 src/HOL/Analysis/Analysis.thy
--- 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
 
diff -r f95193669ad7 -r 1afcfb7fdff4 src/HOL/Analysis/Multivariate_Analysis.thy
--- /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