src/HOL/Library/List_lexord.thy
changeset 37765 26bdfb7b680b
parent 37474 ce943f9edf5e
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Library/List_lexord.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -62,10 +62,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
     1.8 +  "(inf \<Colon> 'a list \<Rightarrow> _) = min"
     1.9  
    1.10  definition
    1.11 -  [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.12 +  "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.13  
    1.14  instance
    1.15    by intro_classes