Hi Tjark, Am 18.01.2013 um 16:44 schrieb Tjark Weber:
> The new AFP entry on Kleene Algebras contains a metis call > (http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652) > 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. Sure, these things happen with pretty much any tool that performs a heuristic search. There are even (rare) cases where taking out the unused theorems will lead to an unprovable first-order problem (because of incompletenesses in the translation of HO constructs). What's your concrete suggestion here? Cheers, Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
