[isabelle-dev] NEWS -> Redundant lemmas
hoelzl at in.tum.de
Thu Sep 22 16:15:18 CEST 2011
>>> 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
More information about the isabelle-dev