[isabelle-dev] [isabelle] Simplification in locales

[Clemens Ballarin]

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?