# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1597783524 -3600
# Node ID 2d7619fc0e1afd710423703bba7f966574c33724
# Parent  721a05da8fe7d770bd51b84f3404b4f7ca1db551
List_Lexorder finally working

diff -r 721a05da8fe7 -r 2d7619fc0e1a src/HOL/Library/List_Lexorder.thy
--- 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