[opentheory-users] Importing proofs of version 6

[Joe Leslie-Hurd]

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
>
>