src/HOL/Analysis/Ordered_Euclidean_Space.thy

--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Dec 26 20:57:23 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Dec 27 19:48:28 2018 +0100
@@ -145,7 +145,7 @@
 qed
 
 lemma%unimportant (in order) atLeastatMost_empty'[simp]:
-  "(~ a <= b) \<Longrightarrow> {a..b} = {}"
+  "(\<not> a \<le> b) \<Longrightarrow> {a..b} = {}"
   by (auto)
 
 instance real :: ordered_euclidean_space