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