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
considerations here.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
