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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
