[isabelle-dev] NEWS -> Redundant lemmas
lp15 at cam.ac.uk
Thu Sep 22 11:33:08 CEST 2011
I think this is a good idea.
On 22 Sep 2011, at 03:08, Brian Huffman 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?
More information about the isabelle-dev