src/HOL/ex/ThreeDivides.thy
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-03-01 krauss 2010-03-01 more recdef (and old primrec) hunting
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-10-20 wenzelm 2009-10-20 tuned header;
2009-02-18 huffman 2009-02-18 speed up proof of exp_exists
2008-09-01 nipkow 2008-09-01 renamed lemma
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-03 wenzelm 2007-06-03 tuned document;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
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