Re: [isabelle] s/h: bogus proofs from e

A problem I’ve often noticed is that meson proofs fail, but replacing “meson” by “metis” creates a working proof.


> On 4 Jul 2021, at 15:09, Tobias Nipkow <nipkow at> wrote:
> I have noticed a similar problem recently, but associated more with meson and verit. Unfortnately I cannot provide a conctrete example right now and cannot say if add_diff_cancel_left' has anything to do with it, but arithmetic is certainly involved.

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