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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
