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

Tjark Weber webertj at in.tum.de
Fri Jan 18 16:44:58 CET 2013


The new AFP entry on Kleene Algebras contains a metis call
that generates a warning about an unused theorem local.opp_mult_def.
Not passing opp_mult_def as an argument to metis gets rid of the
warning, but increases run-time of this metis call from ~ 1 s to ~ 15 s
on my machine.

Best regards,

More information about the isabelle-dev mailing list