[isabelle-dev] NEWS -> Redundant lemmas

[Johannes Hoelzl]

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