Email Gateway (Aug 22 2022 at 16:12): Email Gateway (Aug 22 2022 at 16:12):From: Ognjen Maric <ognjen.maric@gmail.com>
Hi Jasmin,
Ooops - I didn't even realize it was just a text file, I assumed it was
going to be a binary from the size. Anyways, yes - it was MaSh, after
copying the old mash_state over all the proofs are found again. So as a
data point, MaSh does help a lot in my case :)
Thanks,
Ognjen
Email Gateway (Aug 22 2022 at 16:20):From: Ognjen Maric <ognjen.maric@gmail.com>
Dear list,
in playing around with Isabelle2017-RC3 I noticed that Sledgehammer
fails to find some proofs that the 2016 version did (in about 5/10 cases
that I tried). Is this a normal consequence of a fresh MaSh
installation? Can I just copy the old mash_state over (it's about twice
the size of the new one)? I like my automated proofs :)
Cheers,
Ognjen
Last updated: May 06 2024 at 16:21 UTC