[isabelle-dev] Sledgehammer error involving Vampire

Larry Paulson lp15 at cam.ac.uk
Sat Jul 18 23:24:46 CEST 2015

Previous message (by thread): [isabelle-dev] NEWS: Subgoal.FOCUS combinators use anonymous quasi-bound variables
Next message (by thread): [isabelle-dev] Sledgehammer error involving Vampire
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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”)

~/isabelle/Repos/src/HOL: hg id
4050b243fc60 tip

Larry

Previous message (by thread): [isabelle-dev] NEWS: Subgoal.FOCUS combinators use anonymous quasi-bound variables
Next message (by thread): [isabelle-dev] Sledgehammer error involving Vampire
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list