[isabelle-dev] sledgehammer issues

[Lawrence Paulson]

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  
an apply-proof.
Larry

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.
>
> Larry
>