[isabelle-dev] Interpretation in arbitrary targets.
florian.haftmann at informatik.tu-muenchen.de
Wed Mar 27 22:27:20 CET 2013
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev