Hi Johannes, You could define the syntax for has_integral to be literally

## Advertising

"(f Bochner.has_integral x) s"

`and similarly for the other. Additionally, you could declare bundles with the existing`

`notation`

"(f has_integral x) s"

`for both of them (like is nowadays done for the Lifting package syntax). Then, you can`

`locally include the notation for the desired integral with "includes", which is more`

`flexible than a locale interpretation.`

Andreas On 08/08/16 16:57, Johannes Hölzl wrote:

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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev