src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
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
14 months ago paulson 2018-04-28 getting rid of "defer"
15 months ago nipkow 2018-04-26 new simp modifier: reorient
15 months ago paulson 2018-04-17 Change of variables proof
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 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-09 merged
15 months ago paulson 2018-04-09 A couple of new results
15 months ago nipkow 2018-04-09 removed dots at the end of (sub)titles
17 months ago paulson 2018-02-25 new material on matrices, etc., and consolidating duplicate results about of_nat
17 months ago immler 2018-02-22 merged
17 months ago immler 2018-02-22 moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
17 months ago paulson 2018-02-21 Lots of new material about matrices, etc.
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
18 months ago paulson 2018-01-08 moved in some material from Euler-MacLaurin
21 months ago paulson 2017-10-19 Switching to inverse image and constant_on, plus some new material
21 months ago paulson 2017-10-09 new material about connectedness, etc.
21 months ago paulson 2017-09-29 Merge (resolved trivial conflict)
21 months ago paulson 2017-09-29 New results for Green's theorem
22 months ago paulson 2017-08-31 more proof simplificaition
22 months ago paulson 2017-08-30 eliminated some goal_cases
22 months ago paulson 2017-08-30 unscrambled has_integral_Union
23 months ago paulson 2017-08-29 last-minute integration unscrambling
23 months ago paulson 2017-08-28 final cleanup of negligible_standard_hyperplane and other things
23 months ago paulson 2017-08-28 sorted out cases in negligible_standard_hyperplane
23 months ago paulson 2017-08-28 Unscrambling continues as far as negligible_standard_hyperplane
23 months ago paulson 2017-08-28 unscrambled has_integral_restrict_open_subinterval
23 months ago paulson 2017-08-28 Giant cleanup of fundamental_theorem_of_calculus_interior
23 months ago paulson 2017-08-28 work on indefinite_integral_continuous_left, etc.
23 months ago paulson 2017-08-27 some tidying of division_of_nontrivial
23 months ago paulson 2017-08-27 division_of_nontrivial partial cleanup
23 months ago paulson 2017-08-26 Elimination of some "presume"
23 months ago paulson 2017-08-26 unscrambled Henstock_lemma_part1
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-25 unscrambling of integrable_alt
23 months ago paulson 2017-08-24 work on integrable_alt, etc.
23 months ago paulson 2017-08-24 tidying up has_integral'
23 months ago paulson 2017-08-24 more elimination of "guess", etc.
23 months ago paulson 2017-08-24 Merge (non-trivial)
23 months ago paulson 2017-08-23 More tidying, and renaming of theorems
23 months ago paulson 2017-08-23 More tidying up of monotone_convergence_interval
23 months ago haftmann 2017-08-23 dedicated local for "operative" avoids namespace pollution
23 months ago paulson 2017-08-23 more on the dreadful monotone_convergence_interval
23 months ago paulson 2017-08-15 tidying up henstock_lemma
23 months ago paulson 2017-08-15 tackling another nightmare proof
23 months ago paulson 2017-08-14 patching the previous commit
23 months ago paulson 2017-08-14 further Hensock tidy-up
23 months ago paulson 2017-08-13 further tidying
23 months ago paulson 2017-08-13 general rationalisation of Analysis
23 months ago paulson 2017-08-12 cleanup of integral_norm_bound_integral
23 months ago paulson 2017-08-11 more Henstock_Kurzweil_Integration cleanup
23 months ago paulson 2017-08-10 even more horrible proofs disentangled
23 months ago paulson 2017-08-09 fundamental_theorem_of_calculus_interior: more cleanup
23 months ago paulson 2017-08-09 more cleanup of fundamental_theorem_of_calculus_interior
23 months ago paulson 2017-08-08 more cleanup of fundamental_theorem_of_calculus_interior