Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer



>> "remote_vampire": Internal error:
>> exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML")
> 
> Yes, this is an error raised by Isabelle/HOL 2015...
> 
> I think that this has been pointed out by some other users of Isabelle. Well, I guess so?

Indeed. And this is corrected in the repository version.

The problem with SystemOnTPTP (the online service upon which Sledgehammer relies) is that they aggressively update versions of provers and remove the old versions. Here, the new Vampire produced proofs in a slightly different format, which produced an error.

The list of provers tried can be changed; see the Sledgehammer manual for details.

Jasmin





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