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

Reply via email to