src/HOL/ex/HarmonicSeries.thy
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2015-12-26 wenzelm 2015-12-26 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-10-06 wenzelm 2015-10-06 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-29 wenzelm 2014-04-29 proper Unix line termination;
2014-03-19 hoelzl 2014-03-19 further renaming in Series
2014-03-18 huffman 2014-03-18 adapt to Isabelle/c726ecfb22b6
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2010-05-11 hoelzl 2010-05-11 Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
2010-02-23 huffman 2010-02-23 adapt to changes in simpset
2009-11-07 webertj 2009-11-07 Turned sections into subsections (better document structure).
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s