<div dir="ltr">You can also use the -o or --output option instead of shell redirection.<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Nov 24, 2013 at 2:46 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Ramana,<div><br><div><div class="im"><div>On 24 Nov 2013, at 09:45, Ramana Kumar wrote:</div>

<br><blockquote type="cite"><div dir="ltr"><div>I think the idea of the base package is that everything in it should already be supported by your theorem prover, so you don't need to import it - rather, you use it as a dependency for things you export from your theorem prover.<br>



<br></div></div></blockquote></div>I want to import it so I can have a better look at it. The kind of thing I want to do is to make sure that my reader can prove all the assumptions in it and to make sure that my writer only uses definitions and theorems that it provides when it is writing out a ProofPower inference as a sequence of OpenTheory inferences.</div>

<div><div class="im"><br><blockquote type="cite"><div dir="ltr">That said, I think you can generate a single article that performs all the proofs in a package, like base, using the opentheory tool with the info command and the --article option.<br>

</div><div class="gmail_extra">

<br></div></blockquote></div>I invoked opentheory like this:</div><div><br></div><div><span style="white-space:pre-wrap"> </span>opentheory info --article base</div><div><br></div><div>and after 12 minutes learnt that I should have invoked it like this:</div>

<div><br></div><div><span style="white-space:pre-wrap"> opentheory info --article base</span> >base.art</div><div><br></div><div>I am then able to import all 1117 theorems and 3 assumptions from base.art into ProofPower.</div>

</div><div><br></div><div>Thanks!</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Rob.</div><div><br></div></font></span></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>