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
E.g. see finfun_syntax vs. no_finfun_syntax.
isabelle-dev mailing list