[isabelle-dev] Shadowing of theorem names in locales
makarius at sketis.net
Wed Oct 10 16:57:52 CEST 2012
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
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.
More information about the isabelle-dev