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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
