[isabelle-dev] Shadowing of theorem names in locales

Clemens Ballarin ballarin at in.tum.de
Fri Jan 10 20:34:48 CET 2014

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.


More information about the isabelle-dev mailing list