Re: [isabelle] sledgehammer+vampire 4.0 often fails
> 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
prem_role = Conjecture,
prem_role = Hypothesis,
and rebuild the HOL image:
./bin/isabelle build -b HOL
This archive was generated by a fusion of
Pipermail (Mailman edition) and