[isabelle-dev] NEWS -> Redundant lemmas

[Alexander Krauss]

On 09/22/2011 09:00 PM, Lawrence Paulson wrote:
> I think we are taking this idea too far.
>
> The original suggestion was simply to move deprecated theorem
> bindings into a separate file, where they could be loaded if
> necessary to save people the trouble of having to edit their
> theories.

But people will have to edit their theories anyway, for other reasons
(changed commands, changed theory names, changed tool behaviour/setup,
disappearing or reappearing type constructors :-) ). So this was not
meant as a means for upwards compatibility, but rather of supporting the
upgrade process.

But you are probably right that it is more work than it is worth, at
least at the current state of infrastructure.

Completely different idea: An automated way of checking which theorems
have disappeared from important places (e.g., HOL image) from one
Isabelle version to the next, such that we don't forget them in the
NEWS. This should be straightforward to script.

Alex