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>