[isabelle-dev] NEWS -> Redundant lemmas

Peter Lammich lammich at in.tum.de
Thu Sep 22 11:36:35 CEST 2011

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

More information about the isabelle-dev mailing list