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.

Larry

> On 4 Jul 2021, at 15:09, Tobias Nipkow <nipkow at in.tum.de> 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.