[isabelle-dev] Shadowing of theorem names in locales
florian.haftmann at informatik.tu-muenchen.de
Mon Jun 10 20:40:12 CEST 2013
> I recently tried to make HOL-Algebra compliant to this, but
> unfortunately got stuck in HOL already, where Big_Operators didn't
> comply either (but that's unlikely the only theory).
Yet another unintentional coincidence. If you point we to particular
occurences, I am willing to polish them accordingly.
> If we are serious about forbidding duplicate theorem names eventually we
> probably need to start by introducing a flag to enable/disable this, so
> that it doesn't get introduced by accident to theories where duplicate
> names had already been eliminated.
We did similar things in the past and had some success with it.
> As other have noted before, this is
> not going to be a one-man effort. It is quite a bit of work, but more
> importantly, it involves design decisions (namely whether to rename
> theorems or introduce qualifiers) which is best done by a theory's author.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev