Am Sonntag, den 07.10.2012, 18:06 +0200 schrieb Lars Noschinski: > 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 > relation? > > -- Lars
You are forced to give a name to the subplocale interpretation: sublocale L1 < NAME!: L2 but then it should work. - Johannes _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
