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
Hi Tjark,
Am 11.02.2013 um 12:31 schrieb Tjark Weber:
This continues to be a very minor issue, but perhaps it's still useful
if I share my findings. The good news first: there already is an
attribute to drop the name hint, namely
...[untagged name]
Now the bad news: just like your
Hi Jasmin,
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote:
To suppress the warning, one trick is to ensure that the theorem has no
name hint, e.g.
mythm[THEN asm_rl]
or (if it's not polymorphic) pipe it in with using mythm apply -. The
first trick could be made
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote:
First is quite a bit of work, if you want to bring it into a format
that Joe Hurd can understand, assuming he even has the time to look
into it.
It's probably not worth the effort then. Like you said, this kind of
behavior
On Wed, 30 Jan 2013, Tjark Weber wrote:
Some projects let users vote (+1) on feature requests. Of course, as
Steve Jobs put it: A lot of times, people don't know what they want
until you show it to them.
It is usually better to provide things that people *need*, but that is
even harder to
On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote:
What's your concrete suggestion here?
It's more of a curiosity than an issue, of course. Otherwise, I would
suggest to: First, make sure that the behavior is not due to a bug or
silly inefficiency in the metis code. Second,
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.
