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 descendants, but not in other locale > interpretations?
