Skip to content
Success

Changes

Summary

  1. merged
  2. unscrambling of integrable_alt
  3. renamed s to S to work with previous change
  4. merged
  5. work on integrable_alt, etc.
  6. tidying up has_integral'
  7. more elimination of "guess", etc.
  8. Added lemmas
Changeset 66509:65b6d48fc9a9 by paulson:
merged
Changeset 66508:29d684ce2325 by paulson _lp15@cam.ac.uk_:
unscrambling of integrable_alt
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66507:678774070c9b by paulson _lp15@cam.ac.uk_:
renamed s to S to work with previous change
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
Changeset 66506:c1d8ab323d85 by paulson:
merged
Changeset 66505:b81e1d194e4c by paulson _lp15@cam.ac.uk_:
work on integrable_alt, etc.
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66504:04b3a4548323 by paulson _lp15@cam.ac.uk_:
tidying up has_integral'
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 66503:7685861f337d by paulson _lp15@cam.ac.uk_:
more elimination of "guess", etc.
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
Changeset 66502:5df7a346f07b by nipkow:
Added lemmas
The file was modified src/HOL/List.thy (diff)