[opentheory-users] Porting from HOL Light to HOL?

[Maïssa ELLEUCH]

Hi,



I'm a HOL user and I'm looking for porting the multivariate "Integration"
theory from HOL Light to HOL.

For that, I went through the OpenTheory webpage many times, but I'm not
sure to understand how the tool can

be helpful in this regard. May be, I misunderstood the practical side of
the tool.

Could anyone help me for that?


Thank you very much

Maissa
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121022/7e713a35/attachment.htm>