[isabelle-dev] sledgehammer issues

2007-09-07 Thread 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 versio

[isabelle-dev] sledgehammer issues

2007-09-06 Thread 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