src/HOL/Library/Extended_Nonnegative_Real.thy
2016-10-20 hoelzl 2016-10-20 HOL-Probability: move stopping time from AFP/Markov_Models
2016-10-18 hoelzl 2016-10-18 HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
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-Probability: more about probability, prepare for Markov processes in the AFP
2016-10-01 wenzelm 2016-10-01 clarified lfp/gfp statements and proofs;
2016-09-23 hoelzl 2016-09-23 prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid improper use of "this";
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-04-26 wenzelm 2016-04-26 some uses of 'obtain' with structure statement;
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-15 paulson 2016-03-15 rationalisation of theorem names esp about "real Archimedian" etc.
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 extended nonnegative real numbers