[isabelle-dev] Shadowing of theorem names in locales

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Dec 28 19:53:20 CET 2013

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.



PGP available:
-------------- 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>

More information about the isabelle-dev mailing list