[isabelle-dev] NEWS -> Redundant lemmas

[Peter Lammich]

>> Perhaps we should start using a standardized process for phasing out
>> legacy theorems, like moving them into a separate theory file
>> "Legacy.thy" that would not be imported by default, and would be
>> cleared out after each release. When upgrading Isabelle, users could
>> import Legacy.thy as needed to get their theories working, and then
>> work gradually to eliminate the dependencies on it. What do you think?
>>     

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