Re: [isabelle] Bugreport: sledgehammer confused by lemmas without names



Hi Joachim,

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

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.