On Mon, 8 Oct 2012, Clemens Ballarin wrote:
On the other hand, if theory information is not stored in the internal
name, theory merges can result in invalid locales (that is, locales that
cannot even be activated, leaving alone interpreted).
This is a general principle: global merges of theory date are always
endangered, there is no guarantee that the result works. So it is the
normal order of things, but with the slight modification that for locales
the crash is deferred to the point where the user attempts to use the
result.
Testing well-formedness of merged locales at the theory header is probably
a bit too expensive. We also have a general tendency towards deferred
declarations (e.g. in bundles) so non-strict theory content will occur
more often in the future.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
