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

Reply via email to