[isabelle] [Locales and Duplicate Facts]



Dear all,

I’ve noticed an interesting behavior on locales and duplicate facts: it is
possible to have duplicate facts (same name and result) for the same locale
on different files, but if one tries to make an interpretation of this
locale on a context that imports both files, Isabelle realizes the
duplication and reports an error. This can get even more subtle:  if you
prove a lemma for a locale B and prove that A is a sublocale of B, so if
the fact was already given earlier for A, one gets the same problem only
when trying to instantiate the locale A.

If someone decides to work on this issue, I’m available to help.

Cheers,

Paulo.



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