src/HOL/Series.thy
23 months ago Manuel Eberl 2017-08-20 Various lemmas for HOL-Analysis
23 months ago eberlm 2017-08-17 Replaced subseq with strict_mono
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-07-26 wenzelm 2016-07-26 misc tuning and modernization;
2016-07-02 haftmann 2016-07-02 more theorems
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 paulson 2016-02-23 New and revised material for (multivariate) analysis
2016-02-22 paulson 2016-02-22 An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
2016-02-12 hoelzl 2016-02-12 moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-08 hoelzl 2016-02-08 add type class for topological monoids
2016-01-22 paulson 2016-01-22 Reorganised a huge proof
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-07 wenzelm 2015-12-07 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-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-16 hoelzl 2015-03-16 add inequalities (move from AFP/Amortized_Complexity)
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
2014-11-21 Andreas Lochbihler 2014-11-21 add lemma following a proof suggestion by Joachim Breitner
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-20 hoelzl 2014-10-20 add tendsto_const and tendsto_ident_at as simp and intro rules
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
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