[isabelle-dev] Shadowing of theorem names in locales

[Florian Haftmann]

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

Dito.

	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: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130610/49fe9d02/attachment.sig>