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

[Makarius]

On 08/08/16 17:09, Andreas Lochbihler wrote:
> 
> 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.

It is also possible to 'unbundle' syntax bundles globally. With two
bundles: foo_syntax, no_foo_syntax, it becomes possible to switch back
and forth.

E.g. see finfun_syntax vs. no_finfun_syntax.


	Makarius