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



Hi,

the patch is now on afp-devel (https://foss.heptapod.net/isa-afp/afp-devel/-/commit/27b8976bf077f9dcd9c4f5b5d6ccae4ca872fd1a)
and attached to this email.

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

Simon

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

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?

--
  Peter


On Fri, 2021-11-26 at 21:14 +0100, Makarius wrote:
>
> we now have the pre-final release candidate
>
> https://isabelle.sketis.net/website-Isabelle2021-1-RC4 and AFP has
> also moved
>
> to official ssh://hg at foss.heptapod.net/isa-afp/afp-2021-1

Attachment: sepref.patch
Description: Binary data



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