--- a/src/HOL/Library/List_Lexorder.thy Tue Aug 18 17:38:51 2020 +0100
+++ b/src/HOL/Library/List_Lexorder.thy Tue Aug 18 21:45:24 2020 +0100
@@ -82,7 +82,7 @@
lemma Nil_le_Cons [simp]: "[] \<le> x"
unfolding list_le_def by (cases x) auto
-lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
+lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> (if a = b then x \<le> y else a < b)"
unfolding list_le_def by auto
instantiation list :: (order) order_bot