Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
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 (*>*)
isabelle