[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

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