diff -r b212ee44f87c -r c2465b429e6e src/HOL/Analysis/Starlike.thy --- a/src/HOL/Analysis/Starlike.thy Mon Nov 04 17:59:32 2019 -0500 +++ b/src/HOL/Analysis/Starlike.thy Mon Nov 04 19:53:43 2019 -0500 @@ -8,7 +8,10 @@ chapter \Unsorted\ theory Starlike -imports Convex_Euclidean_Space Abstract_Limits + imports + Convex_Euclidean_Space + Abstract_Limits + Line_Segment begin subsection\Starlike sets\