src/HOL/Library/Library.thy
author chaieb
Tue May 15 18:28:02 2007 +0200 (2007-05-15)
changeset 22981 cf071f3fc4ae
parent 22799 ed7d53db2170
child 23100 1c84d7294d5b
permissions -rw-r--r--
A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;
     1 (* $Id$ *)
     2 (*<*)
     3 theory Library
     4 imports
     5   AssocList
     6   BigO
     7   Binomial
     8   Char_ord
     9   Coinductive_List
    10   Commutative_Ring
    11   Continuity
    12   EfficientNat
    13   Eval
    14   ExecutableRat
    15   Executable_Real
    16   ExecutableSet
    17   FuncSet
    18   GCD
    19   Infinite_Set
    20   MLString
    21   Multiset
    22   NatPair
    23   Nat_Infinity
    24   Nested_Environment
    25   OptionalSugar
    26   Parity
    27   Permutation
    28   Pretty_Char_chr
    29   Pretty_Int
    30   Primes
    31   Quotient
    32   Ramsey
    33   State_Monad
    34   Size_Change_Termination
    35   While_Combinator
    36   Word
    37   Zorn
    38 begin
    39 end
    40 (*>*)