Hi Sascha,<br /><br />Mercurial doesn't work for me, possibly because I downloaded the gzip on 22 Dec.<br /><br />Basically, I get a problem even when I do:<br /><br />lemma "P"<br />sledgehammer<br /><br />Thanks<br />Steve<br /><br />On Jan 6, 2011 3:03pm, Sascha Boehme <boehmes@in.tum.de> wrote:<br />> Hi Steve,<br />> <br />> <br />> <br />> An arbitrary development snapshot of Isabelle is not required to run<br />> <br />> as expected, but many snapshots do.  Since your question is related to<br />> <br />> such an arbitray version of Isabelle, I took the freedom to move your<br />> <br />> question to the developer list.<br />> <br />> <br />> <br />> To solve your issue, could you please specify which precise instance<br />> <br />> of Isabelle you have, e.g., by issuing the command "hg id" at your<br />> <br />> console?  Furthermore, how did the error manifest itself, i.e., under<br />> <br />> what conditions do you see the error?  Do you maybe have a small<br />> <br />> example theory?<br />> <br />> <br />> <br />> Sascha<br />> <br />> <br />> <br />> s.wong.731@gmail.com wrote:<br />> <br />> > Hi all,<br />> <br />> ><br />> <br />> > I'm using the svn version of Isabelle and when I try to run<br />> <br />> > sledgehammer, I get an error complaining that the environment<br />> <br />> > variable "ISABELLE_ATP" is not set. How do I set it? I can't seem to<br />> <br />> > find it in the etc/settings file.<br />> <br />> ><br />> <br />> > Thanks for the help.<br />> <br />> ><br />> <br />> > Steve<br />> <br />>