src/HOL/Analysis/Starlike.thy
changeset 69518 bf88364c9e94
parent 69516 09bb8f470959
child 69529 4ab9657b3257
--- a/src/HOL/Analysis/Starlike.thy	Fri Dec 28 10:29:59 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Dec 28 18:53:19 2018 +0100
@@ -6,10 +6,10 @@
    Author:     Johannes Hoelzl, TU Muenchen
 *)
 
-section \<open>Line segments, Starlike Sets, etc\<close>
+section \<open>Line Segments\<close>
 
 theory Starlike
-  imports Convex_Euclidean_Space
+imports Convex_Euclidean_Space
 begin
 
 subsection \<open>Midpoint\<close>