src/HOL/Library/Extended_Real.thy
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-17 hoelzl 2015-12-17 moved some theorems from the CLT proof; reordered some theorems / notation
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-07 paulson 2015-12-07 Cauchy's integral formula for circles. Starting to fix eventually_mono.
2015-11-23 paulson 2015-11-23 New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
2015-11-11 Andreas Lochbihler 2015-11-11 add lemmas for extended nats and reals
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-09-25 hoelzl 2015-09-25 prove Liminf_inverse_ereal
2015-09-17 wenzelm 2015-09-17 isabelle update_cartouches;
2015-09-13 wenzelm 2015-09-13 renamed method "goals" to "goal_cases" to emphasize its meaning;
2015-09-06 wenzelm 2015-09-06 tuned proofs;
2015-07-23 hoelzl 2015-07-23 Measures form a CCPO
2015-07-23 hoelzl 2015-07-23 reorganized Extended_Real
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-07-14 hoelzl 2015-07-14 add continuous_onI_mono
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-07-03 hoelzl 2015-07-03 generalized sup_continuty of add, ereal_of_enat
2015-07-03 hoelzl 2015-07-03 add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-05-04 hoelzl 2015-05-04 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
2015-04-14 Andreas Lochbihler 2015-04-14 more lemmas about ereal
2015-03-11 hoelzl 2015-03-11 add subadditivity for Liminf on ereal
2015-03-04 nipkow 2015-03-04 Removed the obsolete functions "natfloor" and "natceiling"
2015-01-27 hoelzl 2015-01-27 ereal: tuned proofs concerning continuity and suprema
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2014-12-09 hoelzl 2014-12-09 move topology on enat to Extended_Real, otherwise Jinja_Threads fails
2014-11-21 Andreas Lochbihler 2014-11-21 register pmf as BNF
2014-11-14 hoelzl 2014-11-14 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-10-26 haftmann 2014-10-26 eliminated redundancies; more simp rules
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-08-25 hoelzl 2014-08-25 introduce real_of typeclass for real :: 'a => real
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-30 hoelzl 2014-06-30 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
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)