Re: [isabelle] Sublocale, subclass and execution.

Hi Florian,

> There might be chances for something like
> 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?


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