src/HOL/Library/List_lexord.thy
changeset 52729 412c9e0381a1
parent 38857 97775f3e8722
child 53214 bae01293f4dd
     1.1 --- a/src/HOL/Library/List_lexord.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
     1.5    by (unfold list_le_def) auto
     1.6  
     1.7 -instantiation list :: (order) bot
     1.8 +instantiation list :: (order) order_bot
     1.9  begin
    1.10  
    1.11  definition