[isabelle-dev] Shadowing of theorem names in locales

Lars Noschinski noschinl at in.tum.de
Sun Oct 7 18:06:31 CEST 2012

On 07.10.2012 09:37, Florian Haftmann wrote:
> Hi all,
> currently, theorem names in locales can be shadowed (given that
> declarations are in different theories, otherwise the foundation level
> would reject the declaration since the two foundation theorems would
> have the same name).
> 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.
> Any comments?

How would this interact with sublocale? If two (unrelated) locales 
contain a lemma with the same name, can I still establish a sublocale 

   -- Lars

More information about the isabelle-dev mailing list