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