Summary
- New theory of Equiintegrability / Continuity of the indefinite integral / improper integration
- moved transitive_stepwise_le into Nat, where it belongs
The file was added | src/HOL/Analysis/Improper_Integral.thy |
The file was modified | src/HOL/Analysis/Analysis.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Tagged_Division.thy (diff) |
The file was modified | src/HOL/Analysis/Tagged_Division.thy (diff) |
The file was modified | src/HOL/Nat.thy (diff) |