[isabelle-dev] [isabelle] Simplification in locales

Clemens Ballarin 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
> interpretations?

More information about the isabelle-dev mailing list