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 cleaner through a new attribute, e.g. > "silent" or "nameless".
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" Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
