Re: [isabelle] Best practices for introducing domain specific notation

Count me in as interested in a better (simpler to set up and use) way of managing syntax. For example, there are some infix operators declared in Algebra that in most cases don’t need to be visible outside.


> On 17 May 2019, at 09:55, Alexander Krauss <krauss at> wrote:
> Another interesting question is: What concepts should future-Isabelle
> provide to make this more natural? I find the above pattern quite
> verbose and somewhat unintuitive. Would extensible bundles help?

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.