<table cellspacing="0" cellpadding="0" border="0" ><tr><td valign="top" style="font: inherit;">Hello,<br><br>I am a beginner in Isabelle. <br>I have install Isabelle2007 and have following problem. Plaese help me.<br><br>After starting Proof-General, load a theory and click the button "Use"<br>generates the following message in the minibuffer:<br><br> "Starting process isabelle home/Isabelle2007/bin/isabelle-process -PI -m PGASCII HOL "<br><br>After this nothing happens and when I try to use any other command I get "Proof process busy".<br><br>The same in Isabelle2008 works alright, though, but I need the 2007 version.<br><br>I am using <br><ul><li>Linux 64-bit</li><li>Isabelle2007</li><li> polyml-5.2 <br></li><li>ProofGeneral-3.7.1<br></li></ul><br>Many thanks<br>Lilit </td></tr></table><br>