src/HOL/Library/List_Lexorder.thy
changeset 72169 2d7619fc0e1a
parent 72166 bb37571139bf
child 72184 881bd98bddee
--- 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