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
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
On 09/22/2011 11:36 AM, Peter Lammich 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,
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich 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
On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban urb...@in.tum.de wrote:
I was able to put together replacement theorems for a few of these lemmas:
Inf_singleton ~ Inf_insert [where A={}, unfolded Inf_empty inf_top_right]
Sup_singleton ~ Sup_insert
In Java, there is a deprecated flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the legacy-warnings
it already issues when using some deprecated features (recdef, etc.)
You are assuming that you could flag theorems, and all tools know what
On Thu, Sep 22, 2011 at 6:10 AM, Makarius makar...@sketis.net wrote:
On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
On 09/22/2011 11:36 AM, Peter Lammich wrote:
Perhaps we should start using a standardized process for phasing out
legacy theorems, like moving them into a separate theory file
On 09/22/2011 05:00 PM, Brian Huffman wrote:
I actually like Peter's idea of a deprecated flag better than my
Legacy.thy idea. We might implement it by adding a new deprecated
flag to each entry in the naming type implemented in
Pure/General/name_space.ML. Deprecated names would be treated
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
