[isabelle-dev] Local interpretation [was Interpretation in arbitrary targets.]
Clemens Ballarin
ballarin at in.tum.de
Fri Apr 12 21:04:22 CEST 2013
OK. So, just to make sure that I get this right: for locales A and B
where A contains the theorem a
context B begin
context begin
interpretation x: A
end
theorems b = x.a
end
would enrich B by b but not x.a, right?
Clemens
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?
>
> The interpretation would only affect the inner block.
>
>> - What would be the effect of the entire sequence on B?
>
> None.
>
> In other words, you can think of
>
> context B
> begin
>
> ...
>
> interpretation A
>
> ...
>
> end
>
> being equivalent to
>
> context B
> begin
>
> ...
>
> context
> begin
>
> interpretation A
>
> ...
>
> end
>
> Cheers,
> Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>
More information about the isabelle-dev
mailing list