src/HOL/Complex/ex/HarmonicSeries.thy
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-06-21 wenzelm 2007-06-21 tuned proofs -- avoid implicit prems;
2006-02-19 kleing 2006-02-19 * 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/)