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