[isabelle-dev] Interpretation in arbitrary targets.

[Florian Haftmann]

See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.

When following the suggestions of the ML code
http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42
I am personally still in favor of only three Isar keywords, corresponding to

	permanent_interpretation
	ephemeral_interpretation
	interpret

with the perspective to generalize permanent_interpretation from named
targets to arbitrary targets by means of a dedicated local theory
operation, like Local_Theory.subscription in the previous series of
patches.  But for the moment I will leave this aside anyway.

Cheers,
	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/20130423/0bbc80ab/attachment.sig>