[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?

[Tjark Weber]

Hi Jasmin,

On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote:
> To suppress the warning, one trick is to ensure that the theorem has no
> name hint, e.g.
> 
>     mythm[THEN asm_rl]
> 
> or (if it's not polymorphic) pipe it in with "using mythm apply -". The
> first trick could be made cleaner through a new attribute, e.g.
> "silent" or "nameless".

This continues to be a very minor issue, but perhaps it's still useful
if I share my findings. The good news first: there already is an
attribute to drop the name hint, namely

  ...[untagged "name"]

Now the bad news: just like your suggestion of [THEN asm_rl], this
doesn't get rid of the metis warning, but merely changes it to

  Unused theorems: "??.unknown"

Best regards,
Tjark