[isabelle-dev] Resolve with premises

2013-01-18 Thread Peter Lammich
Hi all, as the question currently arose on the users list, I remembered that I have the following method laying around since several month. I'm using it frequently in apply-style scripts (Mainly to apply induction hypotheses). We discussed here in Munich whether we should add it to Isabelle.

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

2013-01-18 Thread Tjark Weber
Hi, 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

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

2013-01-18 Thread Jasmin Christian Blanchette
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.