src/HOL/Library/Library.thy
author haftmann
Thu May 07 12:17:17 2009 +0200 (2009-05-07)
changeset 31060 75d7c7cc8bdb
parent 30326 a01b2de0e3e1
child 31117 527ba4a37843
permissions -rw-r--r--
added theory for explicit equivalence relation in preorders
     1 (*<*)
     2 theory Library
     3 imports
     4   Abstract_Rat
     5   AssocList
     6   BigO
     7   Binomial
     8   Bit
     9   Boolean_Algebra
    10   Char_ord
    11   Code_Char_chr
    12   Code_Index
    13   Code_Integer
    14   Coinductive_List
    15   Commutative_Ring
    16   Continuity
    17   ContNotDenum
    18   Countable
    19   Determinants
    20   Diagonalize
    21   Efficient_Nat
    22   Enum
    23   Eval_Witness
    24   Executable_Set
    25   Float
    26   Formal_Power_Series
    27   FrechetDeriv
    28   FuncSet
    29   Fundamental_Theorem_Algebra
    30   Infinite_Set
    31   Inner_Product
    32   Lattice_Syntax
    33   ListVector
    34   Mapping
    35   Multiset
    36   Nat_Infinity
    37   Nested_Environment
    38   Numeral_Type
    39   OptionalSugar
    40   Option_ord
    41   Permutation
    42   Pocklington
    43   Poly_Deriv
    44   Polynomial
    45   Preorder
    46   Primes
    47   Product_Vector
    48   Quickcheck
    49   Quicksort
    50   Quotient
    51   Ramsey
    52   Random
    53   Reflection
    54   RBT
    55   State_Monad
    56   Topology_Euclidean_Space
    57   Univ_Poly
    58   While_Combinator
    59   Word
    60   Zorn
    61 begin
    62 end
    63 (*>*)