entry point for analysis without integration theory
authorimmler
Wed, 28 Aug 2019 08:51:20 +0200
changeset 70811 1afcfb7fdff4
parent 70810 f95193669ad7
child 70812 2fb2e7661e16
entry point for analysis without integration theory
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Multivariate_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
 
--- /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