Re: [isabelle] Proof of concept: BNF-based records

So I don't feel so bad anymore about writing syntax translations tgat depend on a configuration flag from the local context ... I did this trick recently to enable advanced syntax in a bundle ... the problem was that some translations that match on the outermost constant of an _expression_ are not supposed to return identity ... this required further workarounds and makes it all feel like a bad hack.


-------- Original Message --------
Subject: Re: [isabelle] Proof of concept: BNF-based records
From: Makarius
To: Peter Lammich
CC: cl-isabelle-users at

On 16/02/18 15:06, Peter Lammich wrote:
>> One important aspect of localizing the record package is actually the
>> concrete syntax. When that is done properly, syntax could be attached
>> to
>> different term constructions, independently of the underlying record
>> representation.
> Is there a way to do advanced syntax (e.g. nonterminal, syntax,
> translations, parse_translation, print_ast_translation) properly (e.g.
> localized)?

Yes, one merely needs to connect local entities with global items in the
background theory (the so-called foundation), according to the usual
policies of local_theory contexts.

Here the foundation consists of raw syntax and translations, and the
connection might require further tricks that have not been used before.

The whole localization business is about such tricks -- to make things
possible that look impossible at first sight.


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