[isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

Recently in private discussion there was the question what the supposed
future of permanent_interpretation is supposed to be.

It looks as follows:
Step 1)
	* Put »permanent_interpretation« into Pure directly.
Step 2)
	* Careful revisiting of the documentation to emphasize the presence of
permanent_interpretation.
	* »permanent_interpretation« as leading construct in the distribution
and the AFP as far as appropriate
Step 3)
	* Discontinue theory-global »interpretation«, which then is just a
degenerated form of »permanent_interpretation«.
	* Discontinue locale-level »sublocale«, which then is just a
degenerated form of »permanent_interpretation«.

There will definitely be one release to breath between step 2 and step 3.

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: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151013/b9b8d2de/attachment.asc>