[isabelle-dev] NEWS -> Redundant lemmas

[Lawrence Paulson]

I think this is a good idea.
Larry

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?