<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Joe,<div><br></div><div>Thanks!</div><div><br><div><div>On 31 Jul 2013, at 21:59, Joe Leslie-Hurd wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div>...<br>To export a single theory from the proof logging fork of HOL Light,<br>follow the instructions at<br><br><a href="http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light">http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light</a><br><br></div></blockquote>That's very useful. Are there any analogous instructions for exporting from HOL4?</div><div><br><blockquote type="cite"><div>The initial start_logging command is used to switch on proof logging,<br>which is off by default since most users don't want to export the<br>whole standard theory library.<br></div></blockquote><blockquote type="cite"><div><br>However, that may indeed be exactly what you want, in which case carry<br>out the following two steps:<br><br>cd opentheory<br>make theories<br><br></div></blockquote><div><br></div>At the moment, I am collecting test data, so the more the merrier.<br><blockquote type="cite"></blockquote><br><blockquote type="cite"><div>Then you should see a lot of stuff pile up in opentheory/articles/<br></div></blockquote><br></div><div>It did. Thanks again.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><br></div></body></html>