changeset 71028 | c2465b429e6e |
parent 71026 | 12cbcd00b651 |
child 71172 | 575b3a818de5 |
--- 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 \<open>Unsorted\<close> theory Starlike -imports Convex_Euclidean_Space Abstract_Limits + imports + Convex_Euclidean_Space + Abstract_Limits + Line_Segment begin subsection\<open>Starlike sets\<close>