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.
  10. merged
  11. not ready for release;
  12. updated to cygwin-20170828, which is close to Cygwin 2.8.2-1;
  13. merged
  14. added eta_expansion and its documentation.
  15. More material on infinite sums
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)
Changeset 66531:d9641709f2df by wenzelm:
merged
Changeset 66530:a3a847c4fbdb by wenzelm:
not ready for release;
The file was modified src/Pure/System/isabelle_tool.scala (diff)
Changeset 66529:f39e01e9c489 by wenzelm:
updated to cygwin-20170828, which is close to Cygwin 2.8.2-1;
The file was modified Admin/PLATFORMS (diff)
The file was modified Admin/Windows/Cygwin/Cygwin-Setup.bat (diff)
The file was modified Admin/Windows/Cygwin/README (diff)
The file was modified Admin/components/bundled-windows (diff)
The file was modified Admin/components/components.sha1 (diff)
The file was modified src/Pure/Admin/build_cygwin.scala (diff)
Changeset 66528:65c3c8fc83e4 by nipkow:
merged
Changeset 66527:7ca69030a2af by nipkow:
added eta_expansion and its documentation.
The file was modified src/Doc/Sugar/Sugar.thy (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
Changeset 66526:322120e880c5 by eberlm _eberlm@in.tum.de_:
More material on infinite sums
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Infinite_Set_Sum.thy (diff)