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