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

Makarius 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
>>  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 


More information about the isabelle-dev mailing list