[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis
Lawrence Paulson
lp15 at cam.ac.uk
Mon Aug 8 16:03:23 CEST 2016
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
More information about the isabelle-dev
mailing list