src/HOL/Library/Library.thy
author obua
Sun May 29 12:41:40 2005 +0200 (2005-05-29)
changeset 16109 e8c169d6f191
parent 15731 29ae73d8a84e
child 16908 d374530bfaaa
permissions -rw-r--r--
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.
     1 (*<*)
     2 theory Library
     3 imports
     4   Accessible_Part
     5   Continuity
     6   EfficientNat
     7   FuncSet
     8   Multiset
     9   NatPair
    10   Nat_Infinity
    11   Nested_Environment
    12   OptionalSugar
    13   Permutation
    14   Primes
    15   Quotient
    16   While_Combinator
    17   Word
    18   Zorn
    19   (*List_Prefix*)
    20   Char_ord
    21   List_lexord
    22 begin
    23 end
    24 (*>*)