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

Clemens Ballarin ballarin at in.tum.de
Sun Apr 7 12:59:01 CEST 2013

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?


More information about the isabelle-dev mailing list