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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
A.thy
Description: application/extension-thy
B.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
