>> 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.) _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
