<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">I suspect they have updated Vampire and the new version’s proof format has changed a bit. I have it on my TODO list.<div class=""><br class=""></div><div class="">Jasmin</div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On 18.07.2015, at 23:37, Jason Dagit <<a href="mailto:dagitj@gmail.com" class="">dagitj@gmail.com</a>> wrote:</div><div class=""><div dir="ltr" class=""><br class=""><div class="gmail_extra"><div class="gmail_quote">On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <span dir="ltr" class=""><<a href="mailto:lp15@cam.ac.uk" target="_blank" class="">lp15@cam.ac.uk</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I’ve seen this error consistently in the past week or so. Updating today didn’t help.<br class="">
<br class="">
"remote_vampire": Internal error:<br class="">
exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML”)<br class=""></blockquote><div class=""><br class=""></div><div class="">For what it's worth, I get this too on Isabelle2015 (plus one change to point it at the new URL). </div><div class=""><br class=""></div><div class="">Maybe it's something on the remote end?</div><div class=""><br class=""></div><div class=""><br class=""></div></div></div></div>
_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></div></blockquote></div><br class=""></div></body></html>