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 suggestion of [THEN asm_rl], this
> doesn't get rid of the metis warning, but merely changes it to
>
> Unused theorems: "??.unknown"
Strange, I really had the impression that I had tested this before suggesting
this.
Thankfully, there's a much easier solution:
using [[metis_verbose = false]] by (metis ...)
or, at the top-level,
declare [[metis_verbose = false]]
Don't ask me why I haven't thought of that before. ;)
Cheers,
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
