Re: [isabelle] Definition in locales and interpretation across multiple theories



Dear Andreas,

I have encountered the following problem with locales and
interpretation. Normally, I would expect that theorems and definitions
which are added to some locale are also immediately available in their
interpretations. However, this does not seem to be the case in the
following example.

due to the operational nature of locales, this does not work. I agree, though, that it would be desireable to have such a form of behaviour in the future.

Probably, this is due to the diamond inheritance structure with the
theories. But: Is there some way to tell Isabelle in TestD to add
definitions to the locale loc in TestB to the definitions from TestC
except changing the theory dependencies?

You cannot change an ancestor theory, and TestD only sees one locale "loc". You can either move the interpretation to TestA or TestD, or declare the missing interpreted theorems from TestB in TestD manually.

Clemens







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