[isabelle-dev] Shadowing of theorem names in locales
makarius at sketis.net
Wed Oct 10 17:00:07 CEST 2012
On Mon, 8 Oct 2012, Johannes Hölzl wrote:
> You are forced to give a name to the subplocale interpretation:
> sublocale L1 < NAME!: L2
> but then it should work.
The auxiliary NAME prefix can be non-mandatory as well, without the "!".
In the tuning of theories towards Isabelle/28e37eab4e6f I've done this
several times already. (I've found it hard to invent good auxiliary
prefixes, but they hardly ever show up in the theory body anyway.)
More information about the isabelle-dev