[isabelle-dev] clang error

[Lawrence Paulson]

Thank you for fixing this proof. When I commit changes to simplification (which I often do), I am happy to fix the AFP entries myself. In this case, I was not able to reach the broken proof, even after the problem with linking to clang was fixed. There may still be a problem with running AutoCorres2 on Apple Silicon machines.

Larry

> On 25 Jul 2024, at 08:43, Norbert Schirmer <nschirmer at apple.com> wrote:
> 
> The Ramsey commit in Isabelle broke that proof. See here.
> 
> changeset:   14717:a4c2d293808e
> tag:         tip
> user:        Norbert Schirmer <nschirmer at apple.com>
> date:        Thu Jul 25 09:37:11 2024 +0200
> summary:     fix proof following Isabelle/e65eed943bee
>