<div dir="ltr">You should look at packages - *package*, <a href="http://www.flownet.com/ron/packages.pdf">http://www.flownet.com/ron/packages.pdf</a></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jul 17, 2014 at 11:40 AM, Gergely Buday <span dir="ltr"><<a href="mailto:gbuday@gmail.com" target="_blank">gbuday@gmail.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="">On 17 July 2014 17:32, Gail Zacharias <<a href="mailto:gz@clozure.com">gz@clozure.com</a>> wrote:<br>


> You're probably in some random package. Try (ccl:quit).<br>
<br>
</div>Thanks. Starting the compiler with scripts/ccl64 I was able to compile<br>
my software and save the image by (save-application). Upon loading it<br>
it does not behave as if it were run from the REPL -- it does not<br>
recognise the definitions that are in theory there. What should I pay<br>
attention for here?<br>
<br>
This is nqthm-1992, an archaic theorem prover. I compiled it according<br>
to its README, then I restarted ccl, loaded nqthm, loaded a proof<br>
script and then I used (save-application).<br>
<span class="HOEnZb"><font color="#888888"><br>
- Gergely<br>
</font></span></blockquote></div><br></div>