[isabelle-dev] sledgehammer issues
lp15 at cam.ac.uk
Fri Sep 7 15:47:08 CEST 2007
Proof reconstruction should be working again.
If you d/l the new Vampire, it too supports proof reconstruction, but
Vampire proofs sometimes contain strange steps, when you'll only get
On 6 Sep 2007, at 16:08, Lawrence Paulson wrote:
> I have just committed a new version with various changes, including
> support for structured proofs with a new version of Vampire. Please
> download a new Vampire binary from http://www.cl.cam.ac.uk/research/
> hvg/Isabelle/atp-linkup.html (Linux only) if you use Vampire.
> The environment variables E_HOME, SPASS_HOME and VAMPIRE_HOME are
> now set automatically in the main settings file. Simplest is if you
> put symblinks to eproof, SPASS and vampire in your $ISABELLE_HOME/
> contrib directory.
> Structured proofs are not working at the moment due to a type
> inference problem. However, apply-proofs should always appear. I
> hope this can be fixed soon.
> There's also a problem that text from the PG output is no longer
> selectable. I'm afraid I have no idea what's going on there.
More information about the isabelle-dev