Re: [isabelle] Definition in locales and interpretation across multiple theories
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and