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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
