[isabelle-dev] Syntax for lattice operations?

[Makarius]

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