<div dir="ltr">Dear Joe,<div><br></div><div>> <span style="font-size:12.8px">I tend to do this kind of work lazily, when someone has a</span></div><span style="font-size:12.8px">demand for it.</span><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">Okay, now I have demand :)</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">Regards,</span></div><div><span style="font-size:12.8px">Robert</span></div><div><span style="font-size:12.8px"><br></span></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 17 September 2015 at 21:04, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br>
<span class=""><br>
> Sorry for not been "alive" for a while.<br>
<br>
</span>Good to have you back :-)<br>
<span class=""><br>
> I noticed that there are some files (in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>) not exported to the base.art<br>
> (mostly things about real numbers). I wonder if there is any reason for<br>
> that.<br>
<br>
</span>The simple answer is that these files have not yet been ported to<br>
OpenTheory, which involves going through each theorem and making sure<br>
that it is provable using the modified HOL Light standard library that<br>
precedes it. I tend to do this kind of work lazily, when someone has a<br>
demand for it.<br>
<span class=""><br>
> Also, I found there is problem downloading opentheory's hol-light.<br>
><br>
> $ git clone <a href="http://src.gilith.com/hol-light" rel="noreferrer" target="_blank">http://src.gilith.com/hol-light</a><br>
<br>
</span>It may have been a temporary connectivity issue - could you please<br>
retry and let me know if you get the same result?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<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" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div><br></div><div>Regards,</div><div>Robert </div><div><br></div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a><br></div><div><span style="font-size:12.8px">New email address at ILLC: </span><a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a><br></div><div><span style="font-size:12px;line-height:20px">Carolina MacGillavrylaan </span><span style="font-size:12px;line-height:20px">2246</span><span style="font-size:12px;line-height:20px"> , 1098 XK AMSTERDAM  HP: </span><span style="color:rgb(20,24,35);font-family:helvetica,arial,sans-serif;font-size:13px;line-height:17.94px;white-space:pre-wrap">0652691901</span><br></div><div><br></div></div></div></div></div></div></div></div></div></div></div></div>
</div>