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 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