Hi Johannes,
You could define the syntax for has_integral to be literally
"(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
