Re: [isabelle] Composing toplevel transitions

> The function/termination package merely needs to expose this in the
> usual way, with after_qed and after_qed_termination arguments in the
> initial function command.

It seems to me that implementing that wouldn't be very complicated.
There are not many occurrences of "Function.*" in the distribution/AFP,
so this might be feasible to do in a day or two. I will investigate this.

> There is certainly a challenge here, because of the loose coupling of
> 'function' and 'termination': termination commands might follow in any
> order and there might be unrelated function/termination commands in
> between. Additional care is required to cope with a potential change of
> local_theory targets between 'function' and 'termination' parts, but
> that situation can already happen in the existing package setup.

That's true. In my case, I'm interacting with the code generator, which
has a global setup anyway. I don't have a good story yet about what I'd
do if the code setup changed in between.


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