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



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

Until your comment, I thought that meson wasn't ignoring "using", but that it was just treating it differently somehow. Now I just convinced myself on a small example that you're probably right. I'll look into it.

Jasmin





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