the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike
authorimmler
Mon, 04 Nov 2019 17:59:32 -0500
changeset 71226 b212ee44f87c
parent 71225 12cbcd00b651
child 71227 c2465b429e6e
the division between Starlike and Convex_Euclidean_Space is artificial, therefore include Starlike
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>