Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names
> For the last lemma, sledgehammer suggests "by (metis )". It seems that
> it finds a proof using the first lemma named x, but cannot print a name
> for it (the single space there is indeed what sledgehammer suggests).
> I’m not sure if such overwriting of a lemma with class should be allowed
> or not, but if it should be allowed then maybe sledgehammer should print
> an error instead.
Thanks for the report! I'll look into this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and