[isabelle-dev] Shadowing of theorem names in locales
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