[isabelle] Interpretation inside locale raises DUP



Dear all,

I would like to report the exceptional behaviour of interpreting a locale inside another locale in Isabelle2013-1. If there is already a global interpretation of the same locale available, the interpretation inside the locale raises the exception DUP in table.ML. I would have expected that the round-up algorithm just ignores duplicate interpretations, as it does for all other combinations of multiple interpretations in locales that I tested. Are my expectations wrong, is this a bug or simply unsupported?

Here's an example:

locale foo

interpretation foo .

locale bar begin

interpretation foo .

*** exception DUP ("Scratch.foo", []) raised (line 358 of "General/table.ML")
*** At command "."

Best,
Andreas




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