[isabelle-dev] NEWS -> Redundant lemmas

[Brian Huffman]

On Thu, Sep 22, 2011 at 11:34 AM, Alexander Krauss <krauss at in.tum.de> wrote:
> For mere renamings or simple generalizations, we should just go ahead,
> making sure that the conversion table is in the NEWS. Having an extra legacy
> phase here only creates extra work with no benefit for anyone. With a new
> release, people usually have to upgrade their theories anyway, so a few
> search/replace items can piggy-back on that work easily and postponing them
> is no better.
>
> The longer legacy process should be only for things that are not as trivial
> for users to replace...

This is a good point. There is only one benefit I can see for having a
legacy phase for renamed theorems: This enables users to make theory
files that are simultaneously compatible with two Isabelle releases.
But this is probably not a big deal.

Anyway, if we are decided that the legacy phase for
renamed/generalized theorems is not useful, then there is no point in
preserving the "legacy theorems" sections in the libraries, is there?
We might as well go ahead and start removing all of these right now
(documenting the removals in the NEWS file, of course).

- Brian