src/HOL/Library/Library.thy
author haftmann
Wed Jan 28 11:04:10 2009 +0100 (2009-01-28)
changeset 29650 cc3958d31b1d
parent 29504 4c3441f2f619
child 29688 6ed9ac8410d8
permissions -rw-r--r--
Reflection.thy now in HOL/Library
     1 (*<*)
     2 theory Library
     3 imports
     4   Abstract_Rat
     5   AssocList
     6   BigO
     7   Binomial
     8   Boolean_Algebra
     9   Char_ord
    10   Code_Char_chr
    11   Code_Index
    12   Code_Integer
    13   Coinductive_List
    14   Commutative_Ring
    15   Continuity
    16   ContNotDenum
    17   Countable
    18   Efficient_Nat
    19   Enum
    20   Eval_Witness
    21   Executable_Set
    22   Float
    23   FuncSet
    24   Infinite_Set
    25   ListVector
    26   Multiset
    27   Nat_Infinity
    28   Nested_Environment
    29   Numeral_Type
    30   OptionalSugar
    31   Option_ord
    32   Permutation
    33   Pocklington
    34   Primes
    35   Quicksort
    36   Quotient
    37   Ramsey
    38   Reflection
    39   RBT
    40   State_Monad
    41   Univ_Poly
    42   While_Combinator
    43   Word
    44   Zorn
    45 begin
    46 end
    47 (*>*)