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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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