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

Tjark Weber webertj at in.tum.de
Sun Jan 20 22:21:49 CET 2013

On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
> What's your concrete suggestion here?

It's more of a curiosity than an issue, of course. Otherwise, I would
suggest to: First, make sure that the behavior is not due to a bug or
silly inefficiency in the metis code. Second, offer a way to suppress
the warning.

Best regards,

More information about the isabelle-dev mailing list