Re: [isabelle] sledgehammer+vampire 4.0 often fails



Dear Christoph,

> I have a problem with sledgehammer in Isabelle 2016 with a recent vampire:
> ...
> Very often (I guess in >50% of the cases), vampire fails like this:
> ...
> Is this a known problem?  Is there anything I can do?

Thank you for your report. This wasn't a known problem; I guess most of us are using an older Vampire.

This will be fixed in the next Isabelle release. If you want to repair your Isabelle locally, change line 535 of

    src/HOL/Tools/ATP/atp_systems.ML

from

   prem_role = Conjecture,

to

   prem_role = Hypothesis,

and rebuild the HOL image:

    ./bin/isabelle build -b HOL

Cheers,

Jasmin





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