src/HOL/Set_Interval.thy

--- a/src/HOL/Set_Interval.thy	Tue May 02 12:51:05 2023 +0100
+++ b/src/HOL/Set_Interval.thy	Tue May 02 15:17:39 2023 +0100
@@ -280,8 +280,8 @@
 context order
 begin
 
-lemma atLeastatMost_empty[simp]:
-  "b < a \<Longrightarrow> {a..b} = {}"
+lemma atLeastatMost_empty[simp]: "b < a \<Longrightarrow> {a..b} = {}" 
+  and atLeastatMost_empty'[simp]: "\<not> a \<le> b \<Longrightarrow> {a..b} = {}"
   by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
 
 lemma atLeastLessThan_empty[simp]: