src/HOL/Analysis/Starlike.thy

--- a/src/HOL/Analysis/Starlike.thy	Thu Dec 05 13:51:09 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Dec 05 18:26:11 2019 +0100
@@ -3842,9 +3842,6 @@
     by (simp add: collinear_subset)
 qed
 
-lemma affine_hull_eq_empty [simp]: "affine hull S = {} \<longleftrightarrow> S = {}"
-  using affine_hull_nonempty by blast
-
 lemma affine_hull_2_alt:
   fixes a b :: "'a::real_vector"
   shows "affine hull {a,b} = range (\<lambda>u. a + u *\<^sub>R (b - a))"