Re: [isabelle] Locale interpretations and imported theories
Quoting Brian Huffman <brianh at cs.pdx.edu>:
On Thu, Jul 9, 2009 at 9:11 AM, Peter
Lammich<peter.lammich at uni-muenster.de> wrote:
I encountered a problem/bug(?) with locales and imported theories.
I have four theories:
def: Defines a locale
add: Adds some lemma to the locale
inst: Interprets the locale, but does *not* import add
use: Imports add and inst
The problem is, that I need to use the added lemma in the
interpretation. However, it is not visible in the theory "use".
This is a long-standing bug in Isabelle's implementation of locales.
It was discussed briefly on the mailing list in February 2008:
I would like to point out that calling this behaviour a bug is jumping
It is conceivable to "round up" interpretations at theory merges, but
note that this will not only populate the new theory with additional
theorems but also with syntax and other declarations. Enabling this
has to be thought through very carefully. I expect it to cause many
more "surprising" effects that will confuse users, hence I'm very
hesitant to provide this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and