src/HOL/Library/Extended_Real.thy
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-19 hoelzl 2014-05-19 introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-09 haftmann 2014-05-09 hardcoded nbe and sml into value command
2014-05-07 hoelzl 2014-05-07 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-04-11 nipkow 2014-04-11 made ereal_add_nonneg_nonneg a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-03-22 haftmann 2014-03-22 generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
2014-03-19 haftmann 2014-03-19 elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
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-03-05 wenzelm 2014-03-05 proper UTF-8;
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-11-12 hoelzl 2013-11-12 better support for enat and ereal conversions
2013-11-12 hoelzl 2013-11-12 equation when indicator function equals 0 or 1
2013-09-25 wenzelm 2013-09-25 tuned proofs;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- less guessing;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-04-25 hoelzl 2013-04-25 revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
2013-04-25 hoelzl 2013-04-25 renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
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-02-20 hoelzl 2013-02-20 move auxiliary lemmas from Library/Extended_Reals to HOL image
2013-02-28 wenzelm 2013-02-28 simplified imports;
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 use order topology for extended reals
2013-01-10 noschinl 2013-01-10 added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-22 wenzelm 2012-03-22 tuned proofs;
2011-12-20 noschinl 2011-12-20 add simp rules for enat and ereal
2011-12-05 hoelzl 2011-12-05 real is better supported than real_of_nat, use it in the nat => ereal coercion
2011-10-21 bulwahn 2011-10-21 replacing metis proofs with facts xt1 by new proof with more readable names
2011-09-21 huffman 2011-09-21 remove redundant instantiation ereal :: power
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-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-02 huffman 2011-09-02 remove redundant lemma reals_complete2 in favor of complete_real
2011-08-25 huffman 2011-08-25 remove duplicate simp declaration
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-07-21 haftmann 2011-07-21 moved some lemmas
2011-07-21 haftmann 2011-07-21 ereal is a complete_linorder instance
2011-07-20 hoelzl 2011-07-20 add code generator setup and tests for ereal
2011-07-19 hoelzl 2011-07-19 rename Fin to enat
2011-07-19 hoelzl 2011-07-19 add ereal to typeclass infinity
2011-07-19 hoelzl 2011-07-19 Rename extreal => ereal