src/HOL/Library/Library.thy
author kleing
Sun Feb 19 13:21:32 2006 +0100 (2006-02-19)
changeset 19106 6e6b5b1fdc06
parent 18397 2d94eb7ff17f
child 19234 054332e39e0a
permissions -rw-r--r--
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)
     1 (*<*)
     2 theory Library
     3 imports
     4   Accessible_Part
     5   BigO
     6   Continuity
     7   EfficientNat
     8   ExecutableSet
     9   FuncSet
    10   Multiset
    11   NatPair
    12   Nat_Infinity
    13   Nested_Environment
    14   OptionalSugar
    15   Permutation
    16   Primes
    17   Quotient
    18   While_Combinator
    19   Word
    20   Zorn
    21   Char_ord
    22   Commutative_Ring
    23   Coinductive_List
    24   ASeries
    25 begin
    26 end
    27 (*>*)