[isabelle-dev] Sledgehammer error involving Vampire

Jason Dagit dagitj at gmail.com
Sat Jul 18 23:37:31 CEST 2015

On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <lp15 at cam.ac.uk> wrote:

> I’ve seen this error consistently in the past week or so. Updating today
> didn’t help.
> "remote_vampire": Internal error:
> exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML”)

For what it's worth, I get this too on Isabelle2015 (plus one change to
point it at the new URL).

Maybe it's something on the remote end?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150718/d899d420/attachment-0002.html>

More information about the isabelle-dev mailing list