[isabelle-dev] Future of permanent_interpretation

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Oct 13 15:13:29 CEST 2015

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« 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.



PGP available:

-------------- 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>

More information about the isabelle-dev mailing list