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

[Jasmin Christian Blanchette]

Hi Tjark,

Am 11.02.2013 um 12:31 schrieb Tjark Weber:

> 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"

Strange, I really had the impression that I had tested this before suggesting this.

Thankfully, there's a much easier solution:

    using [[metis_verbose = false]] by (metis ...)

or, at the top-level,

    declare [[metis_verbose = false]]

Don't ask me why I haven't thought of that before. ;)

Cheers,

Jasmin