Hi Clemens, >> If you point we to particular >> occurences, I am willing to polish them accordingly. > > There are several versions of bounded_iff in the locales of that theory > (and lattice locales from imported theories).
HOL-Complex now builds with strict naming policy for facts (again).
I have stumbled over something which needs some consideration: with
strict naming policy, locales can be compromised by »injecting«
duplicate facts to imported locales. 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.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Strict_Prefix.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
