src/HOL/ex/ThreeDivides.thy
2006-05-27 wenzelm 2006-05-27 tuned;
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib.
2006-02-20 kleing 2006-02-20 fixed
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/)
2006-02-12 wenzelm 2006-02-12 minor tuning of proofs, notably induct;
2006-02-12 kleing 2006-02-12 * moved ThreeDivides from Isar_examples to better suited HOL/ex * moved 2 summation lemmas from ThreeDivides to SetInterval