[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130327/b1b9f715/attachment.sig>