[isabelle-dev] Interpretation in arbitrary targets.

[Clemens Ballarin]

Hi Florian,

OK, then we agree on this.

Please let me know if you need to make changes to locales.ML.  I want  
to make sure that routes out of certain quirks there don't get blocked  
accidentally.

Clemens


Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Hi Clemens,
>
>>> I still see us disagree on how far the local theory game can be driven
>>> wrt. interpretation, nevertheless I can imagine that there is an
>>> intermediate road map which we can agree on:
>>>
>>> * Extend sublocale for use within locale targets s.t.
>>
>> This is fine with me.  Will this work for named targets including
>> classes or just locales?
>
> it will work within locales, and thus within type classes.
>
>>> * Equip interpretation in non-theory targets to allow confined,
>>> non-persistent interpretations.
>>>
>>>   context B
>>>   begin
>>>
>>>   interpretation EXPR
>>>
>>>   end
>>>
>>>   would not add a dependency to B.
>>
>> Here, it's not clear whether the interpretation just wouldn't add a
>> dependency, or wouldn't modify B at all.
>
> It should not modify B at all -- with the restriction that ad-hoc
> contexts currently may leak nontheless in certain situations (cf.
> Makarius' statement).
>
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>