changeset 30663 | 0b6aff7451b2 |
parent 28562 | 4e74209f113e |
child 37474 | ce943f9edf5e |
--- a/src/HOL/Library/List_lexord.thy Mon Mar 23 08:14:23 2009 +0100 +++ b/src/HOL/Library/List_lexord.thy Mon Mar 23 08:14:24 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Library/List_lexord.thy - ID: $Id$ Author: Norbert Voelker *) header {* Lexicographic order on lists *} theory List_lexord -imports Plain "~~/src/HOL/List" +imports List Main begin instantiation list :: (ord) ord