src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
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