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.
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
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.