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

Hi Joachim,

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

just for terminology: there is no »overwriting« of anything, but a
shadowing of (unqualified) names.  The situation is not so artificial,
similar things occur in the Isabelle distribution theories.  However I
have no idea what is going wrong with sledgehammer here.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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