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

[Clemens Ballarin]

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?

Clemens