src/HOL/Limits.thy
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'
2010-04-25 huffman 2010-04-25 define finer-than ordering on net type; move some theorems into Limits.thy
2010-04-25 huffman 2010-04-25 define nets directly as filters, instead of as filter bases
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-06-12 huffman 2009-06-12 add lemma tendsto_setsum
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-06 huffman 2009-06-06 generalize tendsto to class topological_space
2009-06-05 huffman 2009-06-05 put syntax for tendsto in Limits.thy; rename variables
2009-06-04 huffman 2009-06-04 generalize type of 'at' to topological_space; generalize some lemmas
2009-06-02 huffman 2009-06-02 replace filters with filter bases
2009-06-01 huffman 2009-06-01 declare Bfun_def [code del]
2009-06-01 huffman 2009-06-01 simp del -> code del
2009-06-01 huffman 2009-06-01 limits of inverse using filters
2009-06-01 huffman 2009-06-01 add [code del] declarations
2009-05-31 huffman 2009-05-31 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters