Hi Clemens, > I hope, > though, it has become clear that I'm not opposed to having > interpretation in locale contexts by principle, I'm merely opposed to > explaining them in the way you propose.
I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. context B begin sublocale EXPR end is equivalent to sublocale B < EXPR Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80% and more occur with the pattern context B begin … end sublocale B < EXPR context B begin … end * Equip interpretation in non-theory targets to allow confined, non-persistent interpretations. context B begin interpretation EXPR end would not add a dependency to B. Would this make sense? I still think that the frontiers can be pushed further, but this can still be a separate step, on which discussion can be resumed after. 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