--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 10:00:49 2016 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Sep 30 14:05:51 2016 +0100
@@ -8764,12 +8764,6 @@
qed
qed
-lemma rel_frontier_convex_Int_affine:
- fixes S :: "'a::euclidean_space set"
- assumes "convex S" "affine T" "interior S \<inter> T \<noteq> {}"
- shows "rel_frontier(S \<inter> T) = frontier S \<inter> T"
-by (simp add: assms convex_affine_rel_frontier_Int)
-
lemma subset_rel_interior_convex:
fixes S T :: "'n::euclidean_space set"
assumes "convex S"