> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
