[opentheory-users] Importing proofs of version 6

[Robert White]

Thanks for the reply.

I would like to give it a try so I choose option 3 for now. I will use
option 1 to continue my project alongside.

Regards,
Robert

On 3 June 2015 at 22:46, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> Unfortunately I have not yet updated the import capability in my HOL
> Light fork to work with version 6 theories. You can either:
>
> 1. Use the command I showed you before to convert version 6 articles
> to version 5 before importing them.
> 2. Wait for me to implement this functionality.
> 3. Implement it yourself and send me a pull request.
>
> Please let me know what you decide: it may affect the wait time in
> solution 2 :-)
>
> Cheers,
>
> Joe
>
> On Wed, Jun 3, 2015 at 7:58 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > Dear Joe,
> >
> > I noticed that I can't using import for the current version (version 6).
> I
> > am using the one from:
> >
> > git clone http://src.gilith.com/hol-light
> >
> >
> > I wonder if you have implemented it/updated the import.ml file, so I
> won't
> > have to redo your work.
> >
> >
> > Thanks
> >
> > Robert
> >
> >
>



-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150603/a9e9d9c7/attachment.html>