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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
