src/HOL/Limits.thy
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-10 immler 2017-03-10 modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
2017-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2016-10-25 paulson 2016-10-25 more new material
2016-10-18 paulson 2016-10-18 more from moretop.ml
2016-10-17 nipkow 2016-10-17 setprod -> prod
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-09-18 wenzelm 2016-09-18 tuned proofs;
2016-08-25 Manuel Eberl 2016-08-25 More analysis lemmas
2016-07-28 immler 2016-07-28 numerical bounds on pi
2016-07-25 wenzelm 2016-07-25 unused (see 1e9e68247ad1);
2016-07-22 wenzelm 2016-07-22 misc tuning and modernization;
2016-06-14 paulson 2016-06-14 new results about topology
2016-06-09 immler 2016-06-09 approximation, derivative, and continuity of floor and ceiling
2016-05-20 immler 2016-05-20 reduce isUCont to uniformly_continuous_on
2016-05-11 immler 2016-05-11 introduced class topological_group between topological_monoid and real_normed_vector
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 nipkow 2016-02-23 resolved conflict
2016-02-23 nipkow 2016-02-23 more canonical names
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-09 hoelzl 2016-02-09 instantiate topologies for nat, int and enat
2016-02-08 hoelzl 2016-02-08 add type class for topological monoids
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-23 immler 2015-12-23 transfer rule for bounded_linear of blinfun
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 paulson 2015-12-07 Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
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 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
2015-11-02 eberlm 2015-11-02 Rounding function, uniform limits, cotangent, binomial identities
2015-10-29 eberlm 2015-10-29 added many small lemmas about setsum/setprod/powr/...
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-07-14 hoelzl 2015-07-14 generalized filtermap_homeomorph to filtermap_fun_inverse; add eventually_at_top/bot_not_equal
2015-05-07 hoelzl 2015-05-07 generalized tends over powr; added DERIV rule for powr
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-05 paulson 2015-03-05 The function frac. Various lemmas about limits, series, the exp function, etc.
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-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-18 hoelzl 2014-06-18 filters are easier to define with INF on filters.
2014-06-18 hoelzl 2014-06-18 moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros