[opentheory-users] interesting articles

[Ramana Kumar]

On Fri, Jan 14, 2011 at 6:16 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> [I'm replying to the OpenTheory mailing list, since I think your
> question is of general interest.]
>
> I am currently working on some example HOL Light theories that I need
> to support some verified Haskell libraries, the beginnings of which
> can be found in hol-light/opentheory/examples/
>
> However, I think it will be some time before I export any theories
> that expand the HOL4 universe. My future plans include packaging up my
> HOL4 probability theories, which will require the real numbers to be
> packaged, and then the HOL Light complex numbers would be reachable
> and interesting to HOL4 users, but that's some way off. However, your
> idea of building a HOL4 exporter would certainly help with this.

Indeed how would you package the probability theories without a HOL4 exporter?
By porting the script files to HOL-light manually?

>
> Cheers,
>
> Joe
>
> On Thu, Jan 13, 2011 at 4:42 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>> Have you exported any articles for things outside the standard
>> library? Is it easy? (Anything is relatively hard for me since I don't
>> have ocaml installed, but if it's easy to export any theory once I
>> have hol-light installed I might consider doing it myself)
>>
>> I'm thinking of testing my reader on something HOL4 users would
>> actually want. (I'm going to test it on more stdlib stuff first though
>> probably.)
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>