[isabelle-dev] Shadowing of theorem names in locales

[Florian Haftmann]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: A.thy
Type: application/x-extension-thy
Size: 203 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121007/77230608/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: B.thy
Type: application/x-extension-thy
Size: 187 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121007/77230608/attachment-0001.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121007/77230608/attachment.asc>