Re: [isabelle] Export from class target fails to replace operations



Indeed strange.  The mixin in the corresponding class seems somehow get
lost on theory merge.  It will take more rounds of investigation to find
out what is going wrong here.

You can help yourself by introducing a new auxiliary class, cf. B.thy.

	Florian

-- 

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

Attachment: A.thy
Description: application/extension-thy

Attachment: B.thy
Description: application/extension-thy

Attachment: C.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature



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