src/HOL/Library/Extended_Nonnegative_Real.thy
4 months ago haftmann 2019-03-05 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
6 months ago haftmann 2019-01-14 tuned proofs
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
8 months ago haftmann 2018-11-18 removed legacy input syntax
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
10 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
12 months ago nipkow 2018-07-11 (re)moved lemmas
12 months ago paulson 2018-06-28 Generalising and renaming some basic results
13 months ago nipkow 2018-06-07 utilize 'flip'
17 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
17 months ago paulson 2018-02-25 new material on matrices, etc., and consolidating duplicate results about of_nat
17 months ago paulson 2018-02-23 fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
18 months ago nipkow 2018-01-19 added lemma
18 months ago nipkow 2018-01-17 more lemmas by Gouezele
18 months ago nipkow 2018-01-17 move lemmas by Gouezel to distribution
18 months ago wenzelm 2018-01-16 standardized towards new-style formal comments: isabelle update_comments;
18 months ago haftmann 2018-01-13 restored naming of lemmas after corresponding constants
18 months ago wenzelm 2018-01-12 prefer formal comments;
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
21 months ago haftmann 2017-10-30 tuned some proofs and added some lemmas
2017-05-03 paulson 2017-05-03 two new theorems
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2016-10-28 kuncar 2016-10-28 a more general relator domain rule for the function type
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