[isabelle-dev] [isabelle] Simplification in locales
ballarin at in.tum.de
Fri Jul 4 08:50:50 CEST 2008
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.
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
More information about the isabelle-dev