* 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/)
(*<*)
theory Library
imports
Accessible_Part
BigO
Continuity
EfficientNat
ExecutableSet
FuncSet
Multiset
NatPair
Nat_Infinity
Nested_Environment
OptionalSugar
Permutation
Primes
Quotient
While_Combinator
Word
Zorn
Char_ord
Commutative_Ring
Coinductive_List
ASeries
begin
end
(*>*)