On 05/11/2021 10:30, Jasmin Blanchette via Cl-isabelle-users wrote:
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.
You are right, I should have written "seems to be ignoring" because I am not sure myself what exactly is going on. Thanks for taking a look.
Description: S/MIME Cryptographic Signature