[isabelle-dev] Vampire

Lawrence Paulson lp15 at cam.ac.uk
Tue Jul 3 13:07:56 CEST 2018

I keep getting the error message below. I have changed this option many times but it never sticks. It has been happening consistently since yesterday.

~/isabelle/Repos/src/HOL: hg id
ec4fe1032b6e tip


"vampire": Error: The Vampire prover is not activated; to activate it, set the Isabelle system option "vampire_noncommercial" to "yes" (e.g. via
                  the Isabelle/jEdit menu Plugin Options / Isabelle / General)

More information about the isabelle-dev mailing list