[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
webertj at in.tum.de
Mon Feb 11 12:31:46 CET 2013
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
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"
More information about the isabelle-dev