[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Wed Feb 13 09:09:34 CET 2013
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. ;)
More information about the isabelle-dev