src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
6 months ago nipkow 2018-12-27 tuned headers; ~ -> \<not>
8 months ago haftmann 2018-11-22 removed legacy input syntax
8 months ago haftmann 2018-11-18 removed legacy input syntax
8 months ago nipkow 2018-11-11 tuned
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
11 months ago eberlm 2018-08-04 Small lemmas about analysis
12 months ago paulson 2018-06-28 Generalising and renaming some basic results
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 immler 2018-05-03 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
14 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
15 months ago nipkow 2018-04-26 new simp modifier: reorient
15 months ago paulson 2018-04-20 three new theorems
15 months ago paulson 2018-04-17 Change of variables proof
15 months ago paulson 2018-04-17 more about measure
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 paulson 2018-04-14 more new theorems on real^1, matrices, etc.
15 months ago paulson 2018-04-14 a few new theorems and some fixes
15 months ago paulson 2018-04-14 new material about vec, real^1, etc.
15 months ago paulson 2018-04-11 replacement of set integral abbreviations by actual definitions!
15 months ago paulson 2018-04-09 A couple of new results
17 months ago wenzelm 2018-02-15 more symbols;
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
22 months ago paulson 2017-08-31 more proof simplificaition
23 months ago paulson 2017-08-29 last-minute integration unscrambling
23 months ago paulson 2017-08-26 unscrambling esp of Henstock_lemma_part1
23 months ago paulson 2017-08-25 starting to unscramble bounded_variation_absolutely_integrable_interval
23 months ago paulson 2017-08-23 More tidying, and renaming of theorems
23 months ago paulson 2017-08-15 fixed the previous commit (henstock_lemma)
23 months ago paulson 2017-08-13 general rationalisation of Analysis
23 months ago paulson 2017-08-05 final tidying up of lemma bounded_variation_absolutely_integrable_interval
23 months ago paulson 2017-08-05 finally rid of finite_product_dependent
23 months ago paulson 2017-08-05 more cleanup
23 months ago paulson 2017-08-05 trying to disentangle bounded_variation_absolutely_integrable_interval
23 months ago paulson 2017-08-04 more horrible proofs disentangled
23 months ago paulson 2017-08-03 eliminated more "guess", etc.
24 months ago paulson 2017-07-24 refactored some HORRIBLE integration proofs
2017-06-27 paulson 2017-06-27 Removed more "guess", etc.
2017-06-26 paulson 2017-06-26 More tidying of horrible proofs
2017-06-26 paulson 2017-06-26 A few renamings and several tidied-up proofs
2017-06-22 paulson 2017-06-22 New theorems and much tidying up of the old ones
2017-06-21 paulson 2017-06-21 Tidying up integration theory and some new theorems
2017-06-19 paulson 2017-06-19 New theorems; stronger theorems; tidier theorems. Also some renaming
2017-04-27 paulson 2017-04-27 New material (and some tidying) purely in the Analysis directory
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