[isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

On 28 December, 2013 19:53 CET, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: 
 
> HOL-Complex now builds with strict naming policy for facts (again).

Thanks, that's cool.

> I have stumbled over something which needs some consideration: with
> strict naming policy, locales can be compromised by »injecting«
> duplicate facts to imported locales.

That's not cool, but I would say that is a user error.  There are other ways of compromising locales, for example with the sublocale command.

> 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.

I wouldn't want to add special treatment for this.  Currently we can only ensure that a locale is intact by visiting its context.  It would be better if integrity checking could be done in an incremental fashion.  But that would require much more sophistication.

Clemens