[isabelle-dev] NEWS -> Redundant lemmas

[Makarius]

On Thu, 22 Sep 2011, Brian Huffman wrote:

> 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).

My observation is that the (informal) legacy phase for the theory 
libraries is a bit longer than for the ML code base, but that is not a big 
deal.

The cycle for marking things (as done normally in Isabelle/ML) is do add 
the legacy hints *before* a release, and do the purge *after* a release. 
(Big cleanup is general best done in the 2-4 months after a liftoff -- it 
gives a second chance to detect the flaws in the reasoning about "legacy" 
status in the first place.)

Anyway, for this release I think we are getting close to convergence 
pretty soon.  So only the really important things should be finished now.


 	Makarius