<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Ramana,<div><br><div><div>On 24 Nov 2013, at 09:45, Ramana Kumar wrote:</div><br class="Apple-interchange-newline"><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>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><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>I invoked opentheory like this:</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </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 class="Apple-tab-span" style="white-space:pre"> 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><div><br></div><div>Rob.</div><div><br></div></body></html>