# HG changeset patch
# User immler
# Date 1572908372 18000
# Node ID b212ee44f87c0228502968d5e223261471284fc2
# Parent  12cbcd00b651e918b54c9eed39c2c406052b0836
the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike

diff -r 12cbcd00b651 -r b212ee44f87c src/HOL/Analysis/Multivariate_Analysis.thy
--- 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>