On Thu, 10 Mar 2016, Johannes Hölzl wrote:
Alternatively: Would a lattice_syntax locale work nowadays? I remember I
tried it once and for some reason it didn't work. Either notations
aren't supported in locales or they are exported after the context
-block.
The concept of 'bundle' was introduced for that, e.g. to allow "includes
lattice_syntax" for local contexts.
Unfortunately, it is not quite finished: notation within bundles is not
yet supported. It might be relatively easy to do that, but I am presently
working in other corners of the system.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
