src/HOL/Analysis/Multivariate_Analysis.thy
author wenzelm
Thu, 10 Oct 2019 15:18:40 +0200
changeset 70826 63c60df79187
parent 70621 1afcfb7fdff4
child 71027 b212ee44f87c
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
70621
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     1
theory
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     2
  Multivariate_Analysis
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     3
imports
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     4
  Ordered_Euclidean_Space
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     5
  Determinants
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     6
  Cross3
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     7
  Lipschitz
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     8
begin
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
     9
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
    10
text \<open>Entry point excluding integration and complex analysis.\<close>
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
    11
1afcfb7fdff4 entry point for analysis without integration theory
immler
parents:
diff changeset
    12
end