[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Andreas Lochbihler]

Hi Johannes,

You could define the syntax for has_integral to be literally

   "(f Bochner.has_integral x) s"

and similarly for the other. Additionally, you could declare bundles with the existing 
notation

   "(f has_integral x) s"

for both of them (like is nowadays done for the Lifting package syntax). Then, you can 
locally include the notation for the desired integral with "includes", which is more 
flexible than a locale interpretation.

Andreas

On 08/08/16 16:57, Johannes Hölzl wrote:
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>