[isabelle-dev] Syntax for lattice operations?
makarius at sketis.net
Thu Mar 10 11:19:01 CET 2016
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
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.
More information about the isabelle-dev