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

[Clemens Ballarin]

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