[isabelle-dev] NEWS -> Redundant lemmas

[Makarius]

On Thu, 22 Sep 2011, 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.
>
> Of course, we'd also need to invent some interface for marking names as 
> deprecated in the first place. It might also be nice to associate a text 
> string to each deprecated name (perhaps saying what other name/feature 
> to use instead) instead of just using a boolean flag.

This would be the basic plan, but it also needs to be wired up with the 
Prover IDE protocol and stylesheets (which are still only half finished).

The part about the name space is relatively easy, but the "annotation" 
part in the source text requires some further thoughts. Concerning the 
extra text, the attitude in PIDE is to point to the original source for 
additional information.  There could be a semi-formal comment telling the 
user, maybe as simple as the existing "-- cmt" form.  (Some people in 
Edinburgh have proposed "social tagging" :-)

Anyway, I am the one who is responsible for these parts of the system. It 
is old wisdom in Isabelle develoment (with its 25 years) that it is more 
efficient to consult the experts and main responsable persons for each 
particular component, instead of tinkering oneself.  (The latter has 
occasionally happened, either leading to code in terminal condition that 
nobody undertstands anymore, or forcing some poor fellow to re-engineer it 
from the ground up. For the name space module both has happened in 
variations several times already.)


 	Makarius