[isabelle-dev] Interpretation in arbitrary targets.
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sun Apr 14 09:30:46 CEST 2013
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130414/c61a3456/attachment.sig>
More information about the isabelle-dev
mailing list