On 28 December, 2013 19:53 CET, Florian Haftmann <florian.haftm...@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. Clemens _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
