I suspect they have updated Vampire and the new version’s proof format has changed a bit. I have it on my TODO list.
Jasmin > On 18.07.2015, at 23:37, Jason Dagit <dag...@gmail.com> wrote: > > On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <l...@cam.ac.uk > <mailto:l...@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? > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
