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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
