Removes an inconsistent definition from Library.thy ,
authorobua
Sun May 29 12:41:40 2005 +0200 (2005-05-29)
changeset 16109e8c169d6f191
parent 16108 cf468b93a02e
child 16110 c423bb89186d
Removes an inconsistent definition from Library.thy ,
so that the lexical order is the standard order for lists.
The prefix order is not built any more.
src/HOL/Library/Library.thy
     1.1 --- a/src/HOL/Library/Library.thy	Sun May 29 12:39:12 2005 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Sun May 29 12:41:40 2005 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    While_Combinator
     1.5    Word
     1.6    Zorn
     1.7 -  List_Prefix
     1.8 +  (*List_Prefix*)
     1.9    Char_ord
    1.10    List_lexord
    1.11  begin