Re: [isabelle] Sublocale, subclass and execution.

>> context
>>   fixes …
>>   assumes …
>> begin
>> permanent_interpretation …
>> end
> This looks interesting, but it's not clear to me what it would mean.  I take that this is a makeshift context that cannot be entered again.  Presumably the construct yields some sort of lifting?

The idea is that the context itself is embedded into a target again (for
simplicity, let us assume a locale as canonical candidate):

context foo


  fixes …
  assumes P

permanent_interpretation bar: bar …




So, technically speaking, this would establish a sublocale dependency
from bar to foo such that facts propagated from bar to foo gain
additional assumptions P.

It can be seen as a proper user-space pattern to avoid raw instantiation
of foundational facts bar… [OF …].

It is not clear to me whether that machinery can handle this out of the
box (or even properly), so this has to be figured out first.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.