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


I am very interested in the topic.
Our AFP entry (see suffers from
such a problem.
Actually UTP has a very strong syntactic flavor which I would like to
activate and de-activate whenever I want.

I am thinking of an approach that uses a top-level command that allow me to
activate the UTP syntax inside the cartouch and de-activate it whenever I
am out of the scope of the command.
One problem is: it might that my top-level command need the syntax of HOL
as well as the document model "HOL" since I would like to define new
concepts or prove new lemmas with the activated syntax.
But technically I am not sure how practical is this, since I did not yet
start doing it.

I agree that it is not a trivial problem we have here.

Best wishes,


On Fri, May 17, 2019 at 11:24 AM Lawrence Paulson <lp15 at> wrote:

> 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.
> Larry
> > 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.