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 >
