src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
2014-03-18 haftmann 2014-03-18 consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-02-16 wenzelm 2014-02-16 tuned proofs;
2013-11-05 hoelzl 2013-11-05 use INF and SUP on conditionally complete lattices in multivariate analysis
2013-11-05 hoelzl 2013-11-05 use bdd_above and bdd_below for conditionally complete lattices
2013-11-05 hoelzl 2013-11-05 generalize SUP and INF to the syntactic type classes Sup and Inf
2013-09-22 wenzelm 2013-09-22 tuned proofs;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
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 rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-03-05 hoelzl 2013-03-05 move Liminf / Limsup lemmas on complete_lattices to its own file
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-01-31 hoelzl 2013-01-31 use order topology for extended reals
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-09-29 wenzelm 2012-09-29 tuned proofs;
2012-04-25 hoelzl 2012-04-25 moved lemmas to appropriate places
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-20 huffman 2011-09-20 Extended_Real_Limits: generalize some lemmas
2011-09-20 huffman 2011-09-20 add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 noschinl 2011-09-13 tune simpset for Complete_Lattices
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-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-11 huffman 2011-08-11 avoid duplicate rule warnings
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-08-09 huffman 2011-08-09 mark some redundant theorems as legacy
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal
2011-05-23 hoelzl 2011-05-23 move lemmas to Extended_Reals and Extended_Real_Limits
2011-03-14 wenzelm 2011-03-14 standardized headers;
2011-03-14 hoelzl 2011-03-14 reworked Probability theory: measures are not type restricted to positive extended reals
2011-03-14 hoelzl 2011-03-14 split Extended_Reals into parts for Library and Multivariate_Analysis