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 y
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
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 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
behavi
Hi Tjark,
Am 20.01.2013 um 22:21 schrieb Tjark Weber:
> 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
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, of
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.
>
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
