In Java, there is a "deprecated" flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the "legacy"-warnings
it already issues when using some deprecated features (recdef, etc.)
You are assuming that you could flag theorems, and all tools know what
these flags should actually mean, and if they use them.
That's technically quite difficult to achieve.
In principle we have similar flags for name space entries already, e.g.
"concealed". Having an official legacy status (also in the Proper IDE) is
probably easy to implement, but the main work is maintaining the actual
annotations in the libraries. My impression is that the traditional approach
is to clear out old material quickly, so that the issue only arises in a weak
sense. (In contrast, the Java standard library is famous for being strictly
monotonic, where deprecated stuff is never disposed.)
I think theory developers are happy with maintaining the annotations.
Some theories in the distribution already contain a Legacy section (just
grep for Legacy in the *.thy files), adding a deprecation flag would
simplify the maintainance of this and allow us to remove them in a couple
of releases.
- Johannes
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
