Re: [isabelle] Isabelle2021-1-RC4 and afp-2021-1 available for applications (early adopters)

Thanks, I will add it to afp-2021-1.

Please do let me know in general if any afp-devel changes should go into the release version. By default any changes in afp-devel will be ignored for the release.


On 28 Nov 2021, at 01:05, Simon Wimmer <wimmersimon at> wrote:


and attached to this email.

I second that it would be important to have it in the release of afp-2021-1.


Am Fr., 26. Nov. 2021 um 22:23 Uhr schrieb Peter Lammich <lammich at>:

Simon just has fixed a regression introduced into
AFP/Refine_Imperative_HOL, by enforcing context discipline, but not
fixing all places where this new behaviour caused errors.

@Simon: can you submit the patch ASAP?


On Fri, 2021-11-26 at 21:14 +0100, Makarius wrote:
> we now have the pre-final release candidate
> and AFP has
> also moved
> to official ssh://hg at


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