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

[Johannes Hölzl]

Am Montag, den 08.08.2016, 15:03 +0100 schrieb 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.

I would prefer this too,  but has_integral is not a name. It is special
syntax, one writes:   (f has_integral x) s

Either we remove the syntax (and add it to a locale to be interpreted
locally) or rename it. Unfortunately the first option is still
problematic. For example, one needs to setup a context to use it, and
then one is not allowed to enter a locale context.

Another problem is that the theory which gets loaded later is always
slightly preferred as it does not need the theory prefix. Only way to
avoid this would be to hide the theorem names. Or put it in a context
and add the "qualified" command prefix.

Unifying the different names (i.e. integral_minus, sub, diff, uminus,
cmult, mult_left, ...) is also on my TODO list.

 - Johannes