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

Tjark Weber webertj at in.tum.de
Thu Feb 14 12:05:04 CET 2013


Hi Jasmin,

On Wed, 2013-02-13 at 09:09 +0100, Jasmin Christian Blanchette wrote:
> Thankfully, there's a much easier solution:
>     using [[metis_verbose = false]] by (metis ...)
> or, at the top-level,
>     declare [[metis_verbose = false]]

It's always nice to find out that a requested feature already exists.
Thanks again!

Tjark




More information about the isabelle-dev mailing list