Summary
- general rationalisation of Analysis
- merged
- cleanup of integral_norm_bound_integral
The file was modified | src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |
The file was modified | src/HOL/Analysis/Improper_Integral.thy (diff) |
The file was modified | src/HOL/Analysis/Topology_Euclidean_Space.thy (diff) |
The file was modified | src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff) |