[isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]
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
> 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?
More information about the isabelle-dev