[isabelle-dev] Shadowing of theorem names in locales

[Florian Haftmann]

Hi Clemens,

>> If you point we to particular
>> occurences, I am willing to polish them accordingly.
> 
> There are several versions of bounded_iff in the locales of that theory
> (and lattice locales from imported theories).

HOL-Complex now builds with strict naming policy for facts (again).

I have stumbled over something which needs some consideration: with
strict naming policy, locales can be compromised by »injecting«
duplicate facts to imported locales.  This does not exhibit itself until
the compromised locale context is (re-)entered, and I think this is not
desirable.  My first spontaneous thought is that strictness should not
apply during the initialisation of a locale context.

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: Strict_Prefix.thy
Type: application/x-extension-thy
Size: 237 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131228/16bf8395/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131228/16bf8395/attachment.asc>