For further discussion, see now fd4ac1530d63, particulary src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in *isar-ref*.
This goes along the following lines: * »Interpretation« in general is used as generic heading for every kind of intepretation into different destination contexts. * *interpretation* in particular denotes interpretation into a confined context. (The wording in the implementation is not yet consistent, ranging from »epheremal« to »confined«; I have a slight inclination to stick to the latter). *interpret* is the variant for proof blocks. This use of terminology IMHO is consistent with typical uses in mathematics and there had been little debate about that so far. So far for the seemingly non-controversial matter. Concerning the »persistent« / »permanent« / »subscribing« kinds of interpretation, there are two conflicting views so far: * Each local theory can »subscribe« to locales, given that it underlying target implements it. Hence all targets (particularly, global theories and locales) are treated uniformly, using one keyword *permanent_interpretation.* * The user interfaces emphasizes the non-trivial differences between »subscription« into global theories and into locales, particularly the side effects of the latter on the existing locale hierarchy. Personally I have no strong inclination to follow the one or the other and I am happy to abandon the first in favour for the second. However then I also suggest a dedicated keyword for interpretation into global theories: a) *interpretation* would otherwise be strangely overloaded, allowing mixin definitions on the level of global theories but not in other local theories. b) Conceptually it would also be possible to allow »subscribing« interpretation into global theories inside a nested local theory (although it is not clear whether our current implementation is actually suitable for that). Then *theory* … *context* … *begin … interpretation* would be ambiguous. c) Similarly, also a theory itself can be seen as a confined context block, making *theory* … *interpretation* itself ambiguous. Suitable candidates could be *theory_interpretation *or *global_interpreation*. Better suggestions welcome. Of course, the actual replacement would not occur in the upcoming but a later release. On that single matter I want to excite some feedback before continuing. Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev