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.
isabelle-dev mailing list