src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
2017-03-10 immler 2017-03-10 modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
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-29 hoelzl 2016-09-29 HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: move gauges and (tagged) divisions to its own theory file
2016-09-28 paulson 2016-09-28 new material connected with HOL Light measure theory, plus more rationalisation
2016-09-27 paulson 2016-09-27 a few new theorems and a renaming
2016-09-23 hoelzl 2016-09-23 move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
2016-09-23 hoelzl 2016-09-23 prove HK-integrable implies Lebesgue measurable; prove HK-integral equals Lebesgue integral for nonneg functions
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel