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

Joe Leslie-Hurd joe at gilith.com
Thu Sep 17 19:04:38 UTC 2015


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



More information about the opentheory-users mailing list