[isabelle-dev] Shadowing of theorem names in locales

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


 	Makarius


More information about the isabelle-dev mailing list