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 <[email protected]>:
>
>>>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
