the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike
--- a/src/HOL/Analysis/Multivariate_Analysis.thy Mon Nov 04 17:26:20 2019 -0500
+++ b/src/HOL/Analysis/Multivariate_Analysis.thy Mon Nov 04 17:59:32 2019 -0500
@@ -5,6 +5,7 @@
Determinants
Cross3
Lipschitz
+ Starlike
begin
text \<open>Entry point excluding integration and complex analysis.\<close>