Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. final cleanup of negligible_standard_hyperplane and other things
  3. merged
  4. sorted out cases in negligible_standard_hyperplane
  5. Unscrambling continues as far as negligible_standard_hyperplane
  6. unscrambled has_integral_restrict_open_subinterval
  7. merged
  8. Giant cleanup of fundamental_theorem_of_calculus_interior
  9. work on indefinite_integral_continuous_left, etc.
Changeset 66540:1f955cdd9e59 by paulson:
merged
Changeset 66539:0ad3fc48c9ec by paulson _lp15@cam.ac.uk_:
final cleanup of negligible_standard_hyperplane and other things
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66538:6e50b550adf5 by paulson:
merged
Changeset 66537:e2249cd6df67 by paulson _lp15@cam.ac.uk_:
sorted out cases in negligible_standard_hyperplane
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66536:9c95b2b54337 by paulson _lp15@cam.ac.uk_:
Unscrambling continues as far as negligible_standard_hyperplane
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66535:64035d9161d3 by paulson _lp15@cam.ac.uk_:
unscrambled has_integral_restrict_open_subinterval
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66534:9cbe0084b941 by paulson:
merged
Changeset 66533:c485474cd91d by paulson _lp15@cam.ac.uk_:
Giant cleanup of fundamental_theorem_of_calculus_interior
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66532:8a6ce2d9a9f5 by paulson _lp15@cam.ac.uk_:
work on indefinite_integral_continuous_left, etc.
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)