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

[Joe Leslie-Hurd]

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