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