Summary
- merged
- unscrambling of integrable_alt
- renamed s to S to work with previous change
- merged
- work on integrable_alt, etc.
- tidying up has_integral'
- more elimination of "guess", etc.
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Linear_Algebra.thy (diff) |