src/HOL/Analysis/Lebesgue_Measure.thy
6 months ago nipkow 2018-12-28 tuned style and headers
7 months ago eberlm 2018-12-12 Tagged some of HOL-Analysis
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
9 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.
13 months ago nipkow 2018-06-06 reorient -> split; documented split
14 months ago paulson 2018-05-08 tidying more messy proofs
14 months ago nipkow 2018-04-26 new simp modifier: reorient
15 months ago paulson 2018-04-18 tidying up including contributions from Paulo Emílio de Vilhena
15 months ago paulson 2018-04-17 Change of variables proof
15 months ago paulson 2018-04-16 some more random results
15 months ago paulson 2018-04-16 more results about measure and negligibility
15 months ago paulson 2018-04-15 quite a few more results about negligibility, etc., and a bit of tidying up
15 months ago paulson 2018-04-15 a few more results
15 months ago paulson 2018-04-15 various new results on measures, integrals, etc., and some simplified proofs
15 months ago nipkow 2018-04-09 removed dots at the end of (sub)titles
17 months ago paulson 2018-02-19 lots of new material, ultimately related to measure theory
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
19 months ago Manuel Eberl 2017-12-05 Moved material from AFP to Analysis/Number_Theory
2017-06-22 paulson 2017-06-22 New theorems and much tidying up of the old ones
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-26 paulson 2017-04-26 Some fixes related to compactE_image
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-Probability: more about probability, prepare for Markov processes in the AFP
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-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.