Re: [isabelle] Locale interpretations and imported theories



On Thu, 9 Jul 2009, Brian Huffman wrote:

The issue stems from the interaction between two Isabelle features
(locales and theory-merging), so I guess I shouldn't have called it a
bug in the locale package; it could just as well be called a bug in
Isabelle's theory-merging feature.

Theory merge does nothing more than delegate the actual merge operation to theory data provided in user space (here the locale mechanism). So there cannot be a bug "in" Isabelle's theory merge feature, but you could call the whole feature a bug, because it raises delicate questions (which is a well-known fact). But then, "feature" and "bug" are really synonyms, and life can be generally simplified by deleting both words from one's dictionary (which I have done many years ago).

BTW, the locale mechanism is properly called a "target" (of the local theory framework). A "package" is something that implements a specification mechanism that lives within such a target, e.g. 'inductive', 'function', 'primrec'.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.