[isabelle-dev] NEWS -> Redundant lemmas

[Lukas Bulwahn]

On 09/22/2011 11:36 AM, Peter Lammich wrote:
>>> 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?
>>>
If one tries to follow Brian's idea, even with the Legacy.thy, there is 
still no guarantees that by importing the theory, everything works as 
with the release before.
For some incompatible changes, retaining compatibility within another 
theory is larger than the change itself.

But for the special case of phasing out legacy theorems, it might work, 
but then I would only restrict this Legacy theory to selected theories 
(maybe everything within HOL-Plain or even less).

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



Lukas