src/HOL/Series.thy
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-02 hoelzl 2014-04-02 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-19 hoelzl 2014-03-19 further renaming in Series
2014-03-18 hoelzl 2014-03-18 fix HOL-NSA; move lemmas
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-17 paulson 2014-03-17 a few new theorems
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-13 haftmann 2013-09-13 tuned proofs
2013-03-26 hoelzl 2013-03-26 Series.thy is based on Limits.thy and not Deriv.thy
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2013-03-22 hoelzl 2013-03-22 clean up lemma_nest_unique and renamed to nested_sequence_unique
2013-01-31 hoelzl 2013-01-31 introduce order topology
2012-12-03 hoelzl 2012-12-03 use filterlim in Lim and SEQ; tuned proofs
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2011-09-05 huffman 2011-09-05 modify lemma sums_group, and shorten proofs that use it
2011-09-05 huffman 2011-09-05 generalize some lemmas
2011-09-04 huffman 2011-09-04 remove redundant lemmas about LIMSEQ
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-18 huffman 2011-08-18 optimize some proofs
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-03-14 hoelzl 2011-03-14 generalize infinite sums
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-05-03 huffman 2010-05-03 remove unneeded constant Zseq
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2009-11-09 wenzelm 2009-11-09 eliminated hard tabulators;
2009-10-28 paulson 2009-10-28 New theory Probability, which contains a development of measure theory
2009-10-05 paulson 2009-10-05 New lemmas connected with the reals and infinite series
2009-09-25 paulson 2009-09-25 New lemmas involving the real numbers, especially limits and series
2009-05-28 huffman 2009-05-28 generalize constants in SEQ.thy to class metric_space
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-03-22 nipkow 2009-03-22 1. New cancellation simprocs for common factors in inequations 2. Updated the documentation
2009-02-24 huffman 2009-02-24 make more proofs work whether or not One_nat_def is a simp rule
2009-02-05 hoelzl 2009-02-05 Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2008-12-29 haftmann 2008-12-29 adapted HOL source structure to distribution layout
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s