[isabelle] Isabelle2017-RC3 and Sledgehammer

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


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