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?

Clemens





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