src/HOL/Library/Extended_Real.thy
11 months ago paulson 2018-06-28 Incorporating new/strengthened proofs from Library and AFP entries
11 months ago wenzelm 2018-06-22 clarified document antiquotation @{theory};
12 months ago nipkow 2018-06-07 utilize 'flip'
12 months ago wenzelm 2018-06-02 more formal comments;
13 months ago paulson 2018-05-06 starting to tidy up Interval_Integral.thy
15 months ago immler 2018-02-26 moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
15 months ago immler 2018-02-22 moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
17 months ago nipkow 2018-01-17 more lemmas by Gouezele
17 months ago wenzelm 2018-01-12 prefer formal comments;
18 months ago wenzelm 2017-11-26 more symbols;
19 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-09-23 hoelzl 2016-09-23 prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-06-02 hoelzl 2016-06-02 move ennreal and ereal theorems from MFMC_Countable
2016-05-25 wenzelm 2016-05-25 isabelle update_cartouches -c -t;
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-14 hoelzl 2016-04-14 Probability: move emeasure and nn_integral from ereal to ennreal
2016-03-17 hoelzl 2016-03-17 more stuff for extended nonnegative real numbers
2016-03-16 paulson 2016-03-16 Contractible sets. Also removal of obsolete theorems and refactoring
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-19 hoelzl 2016-02-19 generalize more theorems to support enat and ennreal
2016-02-10 hoelzl 2016-02-10 Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
2016-02-09 hoelzl 2016-02-09 add tendsto_add_ereal_nonneg
2016-02-09 hoelzl 2016-02-09 instantiate topologies for nat, int and enat
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
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