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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
