[isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]
makarius at sketis.net
Fri Apr 12 22:04:11 CEST 2013
On Sun, 7 Apr 2013, Clemens Ballarin wrote:
> Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
>> 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?
> - What would be the effect of the entire sequence on B?
Side remark here: presently "context begin ... end" is still quite weak in
holding things local within its body. It is somehow a consequence how the
Haftman-Wenzel Neapolitan wafer worked out in the first approach. These
things are not yet set in stone, but we need to keep such fine points in
More information about the isabelle-dev