--- a/src/HOL/Analysis/Homeomorphism.thy Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu Dec 27 19:48:28 2018 +0100
@@ -201,7 +201,7 @@
lemma%unimportant segment_to_rel_frontier:
fixes x :: "'a::euclidean_space"
assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
- and y: "y \<in> S" and xy: "~(x = y \<and> S = {x})"
+ and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
"open_segment x z \<subseteq> rel_interior S"
proof (cases "x=y")