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

[Joe Leslie-Hurd]

Hi Maissa,

The process for doing this porting using OpenTheory is not yet proven,
though I know Ramana Kumar is currently working on importing some HOL
Light theories into HOL4. Probably the best place to start are the
following two questions on the FAQ list:

How can I generate a proof article file from a HOL Light theory file?
http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light

How can I read a proof article file into my theorem prover?
http://www.gilith.com/research/opentheory/faq.html#import-proof-article

Hope that helps - please let me know if you have any difficulties.

Cheers,

Joe

On Mon, Oct 22, 2012 at 3:13 AM, Maïssa ELLEUCH
<maissa.elleuch at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>