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

Robert White ai.robert.wangshuai at gmail.com
Thu Sep 17 18:18:49 UTC 2015

Dear Joe,

Sorry for not been "alive" for a while.
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.

Also, I found there is problem downloading opentheory's hol-light.

$ git clone http://src.gilith.com/hol-light

Cloning into 'hol-light'...

error: Unable to get pack file

Recv failure: Connection reset by peer

error: Unable to find 78e7e5d91a3b45ac7bd2f32939fe575fe0f18a64 under

Cannot obtain needed tree 78e7e5d91a3b45ac7bd2f32939fe575fe0f18a64

while processing commit 9991514634d6ecea96ff4ea3985b069d3c4279ca.

error: fetch failed.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150917/73d376ec/attachment.html>

More information about the opentheory-users mailing list