[opentheory-users] packages that are not exported in hol.ml?

[Robert White]

Dear Joe,

> I tend to do this kind of work lazily, when someone has a
demand for it.

Okay, now I have demand :)

Regards,
Robert


On 17 September 2015 at 21:04, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> > Sorry for not been "alive" for a while.
>
> Good to have you back :-)
>
> > I noticed that there are some files (in hol.ml) not exported to the
> base.art
> > (mostly things about real numbers). I wonder if there is any reason for
> > that.
>
> The simple answer is that these files have not yet been ported to
> OpenTheory, which involves going through each theorem and making sure
> that it is provable using the modified HOL Light standard library that
> precedes it. I tend to do this kind of work lazily, when someone has a
> demand for it.
>
> > Also, I found there is problem downloading opentheory's hol-light.
> >
> > $ git clone http://src.gilith.com/hol-light
>
> It may have been a temporary connectivity issue - could you please
> retry and let me know if you get the same result?
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>



-- 

Regards,
Robert

New homepage at Github: https://airobert.github.io/
New email address at ILLC: shuai.wang at student.uva.nl
Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150917/fa325c97/attachment.html>