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

[Florian Haftmann]

Am 12.04.2013 21:04, schrieb 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?

Not quite.  The example which produces this effect is:

>   context B begin
>     context begin
>       interpretation x: A
>       theorems b = x.a
>     end
>   end

As Makarius pointed out, »hiding« might be imperfect, but wrt. to
interpretation this should not be that difficult to achieve.

	Florian

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130414/49d66221/attachment.sig>