src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
22 months ago paulson 2017-08-24 more elimination of "guess", etc.
22 months ago paulson 2017-08-24 Merge (non-trivial)
22 months ago paulson 2017-08-23 More tidying, and renaming of theorems
22 months ago paulson 2017-08-23 More tidying up of monotone_convergence_interval
22 months ago haftmann 2017-08-23 dedicated local for "operative" avoids namespace pollution
22 months ago paulson 2017-08-23 more on the dreadful monotone_convergence_interval
22 months ago paulson 2017-08-15 tidying up henstock_lemma
22 months ago paulson 2017-08-15 tackling another nightmare proof
22 months ago paulson 2017-08-14 patching the previous commit
22 months ago paulson 2017-08-14 further Hensock tidy-up
22 months ago paulson 2017-08-13 further tidying
22 months ago paulson 2017-08-13 general rationalisation of Analysis
22 months ago paulson 2017-08-12 cleanup of integral_norm_bound_integral
22 months ago paulson 2017-08-11 more Henstock_Kurzweil_Integration cleanup
22 months ago paulson 2017-08-10 even more horrible proofs disentangled
22 months ago paulson 2017-08-09 fundamental_theorem_of_calculus_interior: more cleanup
22 months ago paulson 2017-08-09 more cleanup of fundamental_theorem_of_calculus_interior
22 months ago paulson 2017-08-08 more cleanup of fundamental_theorem_of_calculus_interior
22 months ago paulson 2017-08-08 partly unravelled fundamental_theorem_of_calculus_interior
22 months ago paulson 2017-08-08 more unknotting
22 months ago paulson 2017-08-07 more Henstock_Kurzweil_Integration cleanup
22 months ago paulson 2017-08-06 more integration cleanups
22 months ago paulson 2017-08-06 further cleanup of "guess"
22 months ago paulson 2017-08-06 towards a cleanup of Henstock_Kurzweil_Integration.thy
22 months ago paulson 2017-07-30 partial cleanup of the horrible Tagged_Division
23 months ago paulson 2017-07-26 New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
23 months ago paulson 2017-07-24 refactored some HORRIBLE integration proofs
24 months ago paulson 2017-06-27 Removed more "guess", etc.
24 months ago paulson 2017-06-26 More tidying of horrible proofs
24 months ago paulson 2017-06-26 A few renamings and several tidied-up proofs
24 months ago paulson 2017-06-22 New theorems and much tidying up of the old ones
24 months ago 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-06-15 paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-05-02 paulson 2017-05-02 Simplification of some proofs. Also key lemmas using !! rather than ! in premises
2017-04-27 paulson 2017-04-27 New material (and some tidying) purely in the Analysis directory
2017-04-25 paulson 2017-04-25 New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
2017-03-10 immler 2017-03-10 modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
2017-02-21 paulson 2017-02-21 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
2017-01-17 wenzelm 2017-01-17 isabelle update_cartouches -c -t;
2017-01-04 paulson 2017-01-04 Many new theorems, and more tidying
2016-10-18 paulson 2016-10-18 more from moretop.ml
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-29 hoelzl 2016-09-29 HOL-Analysis: move gauges and (tagged) divisions to its own theory file
2016-09-28 hoelzl 2016-09-28 HOL-Analysis: add cover lemma ported by L. C. Paulson
2016-09-27 paulson 2016-09-27 a few new theorems and a renaming
2016-09-26 hoelzl 2016-09-26 use filter to define Henstock-Kurzweil integration
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-22 paulson 2016-09-22 More mainly topological results
2016-09-21 paulson 2016-09-21 new material about topological concepts, etc
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-25 Manuel Eberl 2016-08-25 More analysis lemmas
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-08-10 haftmann 2016-08-10 keeping lifting rules local
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.