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
2012-12-03 hoelzl 2012-12-03 add filterlim rules for unary minus and inverse
2012-12-03 hoelzl 2012-12-03 rename filter_lim to filterlim to be consistent with filtermap
2012-11-27 hoelzl 2012-11-27 introduce filter_lim as a generatlization of tendsto
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-12 noschinl 2012-03-12 use eventually_elim method
2012-03-12 noschinl 2012-03-12 add eventually_elim method
2011-12-15 noschinl 2011-12-15 add lemmas about limits
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-20 huffman 2011-09-20 add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;
2011-08-31 huffman 2011-08-31 convert to Isar-style proof
2011-08-28 huffman 2011-08-28 move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-20 huffman 2011-08-20 redefine constant 'trivial_limit' as an abbreviation
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-17 huffman 2011-08-17 add lemma tendsto_compose_eventually; use it to shorten some proofs
2011-08-17 huffman 2011-08-17 add lemma metric_tendsto_imp_tendsto
2011-08-15 huffman 2011-08-15 add lemma tendsto_compose
2011-08-14 huffman 2011-08-14 locale-ize some constant definitions, so complete_space can inherit from metric_space
2011-08-14 huffman 2011-08-14 generalize constant 'lim' and limit uniqueness theorems to class t2_space
2011-08-14 huffman 2011-08-14 consistently use variable name 'F' for filters
2011-08-14 huffman 2011-08-14 generalize lemmas about LIM and LIMSEQ to tendsto
2011-08-08 huffman 2011-08-08 rename type 'a net to 'a filter, following standard mathematical terminology
2011-08-08 huffman 2011-08-08 remove duplicate lemmas
2011-03-14 hoelzl 2011-03-14 generalize infinite sums
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-05-10 huffman 2010-05-10 minimize imports
2010-05-04 huffman 2010-05-04 generalize types of LIMSEQ and LIM; generalize many lemmas
2010-05-03 huffman 2010-05-03 add lemmas eventually_nhds_metric and tendsto_mono
2010-05-03 huffman 2010-05-03 remove unneeded premise
2010-05-03 huffman 2010-05-03 add constants netmap and nhds
2010-05-01 huffman 2010-05-01 complete_lattice instance for net type
2010-05-01 huffman 2010-05-01 swap ordering on nets, so x <= y means 'x is finer than y'