--- a/src/HOL/Analysis/Starlike.thy Wed Jan 16 18:14:02 2019 -0500
+++ b/src/HOL/Analysis/Starlike.thy Wed Jan 16 19:34:48 2019 -0500
@@ -5,13 +5,14 @@
Author: Armin Heller, TU Muenchen
Author: Johannes Hoelzl, TU Muenchen
*)
-
-section \<open>Line Segments\<close>
+chapter \<open>Unsorted\<close>
theory Starlike
imports Convex_Euclidean_Space
begin
+section \<open>Line Segments\<close>
+
subsection \<open>Midpoint\<close>
definition%important midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"