[isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]
florian.haftmann at informatik.tu-muenchen.de
Tue Apr 9 20:24:03 CEST 2013
>> context B begin
>> interpretation A
> This looks attractive, but could you please elaborate the semantics:
> - What would be the effect of the interpretation from the inner block on
> the outer block?
The interpretation would only affect the inner block.
> - What would be the effect of the entire sequence on B?
In other words, you can think of
being equivalent to
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev