[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

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.)


 	Makarius