[isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]

[Makarius]

On Sun, 7 Apr 2013, Clemens Ballarin wrote:

> Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
>
>> context B begin
>>  context
>>  begin
>>    interpretation A
>>  end
>> end
>
> 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 
mind.


 	Makarius