src/HOL/Library/List_Lexorder.thy
changeset 72169 2d7619fc0e1a
parent 72166 bb37571139bf
child 72184 881bd98bddee
equal deleted inserted replaced
72168:721a05da8fe7 72169:2d7619fc0e1a
    80   unfolding list_le_def by (cases x) auto
    80   unfolding list_le_def by (cases x) auto
    81 
    81 
    82 lemma Nil_le_Cons [simp]: "[] \<le> x"
    82 lemma Nil_le_Cons [simp]: "[] \<le> x"
    83   unfolding list_le_def by (cases x) auto
    83   unfolding list_le_def by (cases x) auto
    84 
    84 
    85 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
    85 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> (if a = b then x \<le> y else a < b)"
    86   unfolding list_le_def by auto
    86   unfolding list_le_def by auto
    87 
    87 
    88 instantiation list :: (order) order_bot
    88 instantiation list :: (order) order_bot
    89 begin
    89 begin
    90 
    90