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

[Tjark Weber]

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

> To suppress the warning, one trick is to ensure that the theorem has no
> name hint, e.g.
> 
>     mythm[THEN asm_rl]

Good to know that there is a workaround.

> [*] A rule of thumb I remember from industry was to wait until we had
> the same feature request at least three times before implementing
> anything. That of course made more sense w.r.t. a large user base (~ 10
> 000 to 100 000) than for the Isabelle community.

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

Best regards,
Tjark