[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Lawrence Paulson]

Thank you for making this change!

> My idea would be to rename both integrals into something like:
>   has_bc_integral, bc_integrable, bc_integral,
>   has_hk_integral, hk_integrable, hk_integral
> and consequently rename the integral theorems.

I would greatly prefer renaming the relevant theories instead so that we have Bochner.has_integral versus Gauge.has_integral, etc. That is the point of having compound names. I would go so far as to suggest that equivalent theorems with slightly different names should be rationalised.

Larry