[isabelle-dev] Shadowing of theorem names in locales

[Peter Lammich]

The same may happen with constants, and I was already confused several
times, when the interpretation command failed due to this effect. Using
locale expressions and forgetting to add name prefixes (a!:, b!:, etc)
can easily cause this effect.

So I also vote for an error message (or at least a warning) that occurs
immediately when defining the locale or the constant/lemma inside a
locale.

Peter


On So, 2012-10-07 at 09:37 +0200, 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?
> 
> Cheers,
> 	Florian
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev