[isabelle-dev] Interpretation in arbitrary targets.
makarius at sketis.net
Thu Mar 28 13:31:16 CET 2013
On Wed, 27 Mar 2013, Florian Haftmann wrote:
> After one further round of thinking, I would still suggest
> * »interpretation« for interpretation without subscription
> * »subscription« for interpretation with subscription
> I think it is worth to distinguish these on the surface. Maybe future
> will bring different possibilities with »private« or whatever. But
> interpretation is still rare enough that one further change of surface
> syntax is not that tremendous to end users.
Right now we should merely have clear terminology in the discussion. The
language keywords can be finalized later.
Note that 'interpret' within a local proof context is also without
subscription -- as a consequence of how that works.
I also agree with you now that 'private' should be just about superficial
name space issues (potentially with notation, i.e. things of the
"syntax_declaration" category). So it can stay outside of the
More information about the isabelle-dev