[isabelle-dev] NEWS -> Redundant lemmas
makarius at sketis.net
Fri Sep 23 00:10:02 CEST 2011
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
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.
More information about the isabelle-dev