[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

On Sun, 7 Oct 2012, Florian Haftmann wrote:

> After some pondering I would argue that this should be forbidden:
> * (Complete) shadowing is a constant source of confusion.
> * Global interpretations are impossible then, since they would result in
> two global theorems with the same name.

I've started some experiments with this idea and will report the empirical 
results soon ...


 	Makarius