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




On 13/07/2021 10:59, Jasmin Blanchette via Cl-isabelle-users wrote:
Hi Asta,

I find that meson is very sensitive to "using" lemmas vs feeding them as arguments and that sledgehammer ignores this.

Thank you for your report. Thanks to your example, I was able to track down the issue and find a solution for the Isabelle development version.

Somewhat belatedly: Why does meson ignore "using"? Shouldn't it take it into account like metis, simp etc? Does anybody feel responsible for meson?

Tobias

Cheers,

Jasmin


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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