[isabelle-dev] sledgehammer issues
lp15 at cam.ac.uk
Thu Sep 6 17:08:33 CEST 2007
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
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