[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,
Tjark
More information about the isabelle-dev
mailing list