[isabelle-dev] Shadowing of theorem names in locales

Makarius makarius at sketis.net
Tue Oct 9 16:47:41 CEST 2012

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


More information about the isabelle-dev mailing list