src/HOL/Library/Library.thy
author haftmann
Fri Jul 18 18:25:56 2008 +0200 (2008-07-18)
changeset 27652 818666de6c24
parent 27475 61b979a2c820
child 28098 c92850d2d16c
permissions -rw-r--r--
refined code generator setup for rational numbers; more simplification rules for rational numbers
     1 (* $Id$ *)
     2 (*<*)
     3 theory Library
     4 imports
     5   Abstract_Rat
     6   AssocList
     7   BigO
     8   Binomial
     9   Boolean_Algebra
    10   Char_ord
    11   Code_Char_chr
    12   Code_Index
    13   Code_Integer
    14   Code_Message
    15   Coinductive_List
    16   Commutative_Ring
    17   Continuity
    18   Countable
    19   Dense_Linear_Order
    20   Efficient_Nat
    21   Enum
    22   Eval
    23   Eval_Witness
    24   Executable_Set
    25   "../Real/Float"
    26   FuncSet
    27   Imperative_HOL
    28   Infinite_Set
    29   ListVector
    30   Multiset
    31   NatPair
    32   Nat_Infinity
    33   Nested_Environment
    34   Numeral_Type
    35   OptionalSugar
    36   Option_ord
    37   Permutation
    38   Primes
    39   Quicksort
    40   Quotient
    41   Ramsey
    42   RBT
    43   State_Monad
    44   While_Combinator
    45   Word
    46   Zorn
    47 begin
    48 end
    49 (*>*)