Add a deprecation mechanism

[strub]

[chdoc]

I would like to have at least two places to trigger a deprecation warning:

• importing a theory that has been deprecated
• using a lemma or op that has been deprecated

[strub]

For lemmas, operators, internal theories, it would be easy to add a deprecated keyword. For top-level theories, I am not sure what to do so that a user can mark the while file as deprecated.

[chdoc]

Would it be possible to add a command to mark the enclosing theory as deprecated and make deprecated theory ... (or whatever you envisioned) just syntax for opening a theory and invoking the deprecate command right after?

[strub]

Would it be possible to add a command to mark the enclosing theory as deprecated and make deprecated theory ... (or whatever you envisioned) just syntax for opening a theory and invoking the deprecate command right after?

Yes, this makes sense.

[fdupress]

For deprecating a whole file, an extension change could also do? .ecd

The warning part of the mechanism could also be used to deprecate tactics. (We don't need a source-level mechanism to mark tactics as deprecated.)

Do we want to support deprecating a particular clone of a non-deprecated theory? (In which case, we'll want deprecated clone ....)