Currently not. Internally, a locale happens to be an interpretation
in its decendants.
But note that you could add [cong del] to any interpretations you make.
Clemens
On 3 Jul 2008, at 23:32, John Matthews wrote:
Is there a way to only apply a theorem attribute
inside a locale and its
I agree that the locale abstraction is being violated in this case. Even
if locale-defined constants are implemented as abbreviations, this
should not be apparent to the user. Here's my idea for a possible
remedy: Within the locale, the simplifier should use a congruence rule
that
