[isabelle-dev] NEWS -> Redundant lemmas

[Alexander Krauss]

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
> identically to non-deprecated names, except that looking up a
> deprecated name would cause a legacy warning message to be printed. I
> don't think it would be necessary to modify any other tools or
> packages.

Well... taking this seriously would mean to do this not only for facts 
but for all sorts of name space entries. Packages would then have to 
make sure that the legacy flag is propagated, e.g., from a constant to 
its characteristic theorems (unless otherwise indicated by the user, I 
suppose). This is the same as for the "concealed" flag, which is still 
not handled uniformly throughout the system. Like with conceal, one 
would want to make sure that legacy stuff does not show up in search, or 
is not otherwise suggested to users by the system, e.g. via 
sledgehammer. There is in fact quite a bit of similarity with "concealed".

If one has both "legacy" and "concealed", and possibly more once we get 
serious about modular namespaces (e.g., "private" to limit visibility to 
some scope), it might be worth trying to generalize those to some sort 
of general namespace annotation concept...

>> My impression is that the traditional
>> approach is to clear out old material quickly, so that the issue only arises
>> in a weak sense.

For mere renamings or simple generalizations, we should just go ahead, 
making sure that the conversion table is in the NEWS. Having an extra 
legacy phase here only creates extra work with no benefit for anyone. 
With a new release, people usually have to upgrade their theories 
anyway, so a few search/replace items can piggy-back on that work easily 
and postponing them is no better.

The longer legacy process should be only for things that are not as 
trivial for users to replace...

Alex