src/HOL/Limits.thy
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
2014-04-02 paulson 2014-04-02 new theorem about zero limits
2014-03-31 hoelzl 2014-03-31 add limits of power at top and bot
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-05 hoelzl 2013-11-05 move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
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-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-05-30 wenzelm 2013-05-30 tuned headers;
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces
2013-03-26 hoelzl 2013-03-26 move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 rename RealVector.thy to Real_Vector_Spaces.thy
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
2013-03-22 hoelzl 2013-03-22 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
2013-03-22 hoelzl 2013-03-22 move metric_space to its own theory
2013-03-22 hoelzl 2013-03-22 move topological_space to its own theory
2013-03-06 hoelzl 2013-03-06 add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
2013-02-20 hoelzl 2013-02-20 move auxiliary lemmas from Library/Extended_Reals to HOL image
2013-02-06 hoelzl 2013-02-06 replace open_interval with the rule open_tendstoI; generalize Liminf/Limsup rules
2013-01-31 hoelzl 2013-01-31 introduce order topology
2013-01-14 hoelzl 2013-01-14 move eventually_Ball_finite to Limits
2012-12-07 hoelzl 2012-12-07 add exponential and uniform distributions
2012-12-04 hoelzl 2012-12-04 prove tendsto_power_div_exp_0 * * * missing rename
2012-12-04 hoelzl 2012-12-04 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
2012-12-03 hoelzl 2012-12-03 use filterlim in Lim and SEQ; tuned proofs
2012-12-03 hoelzl 2012-12-03 conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
2012-12-03 hoelzl 2012-12-03 add L'Hôpital's rule
2012-12-03 hoelzl 2012-12-03 add filterlim rules for exp and ln to infinity
2012-12-03 hoelzl 2012-12-03 add filterlim rules for inverse and at_infinity
2012-12-03 hoelzl 2012-12-03 add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image