[isabelle-dev] sledgehammer issues

[Lawrence Paulson]

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.

Larry