[opentheory-users] What's behind the article merging function

[Joe Leslie-Hurd]

Hi Robert,

If you pull the most recent version of the OpenTheory HOL Light fork,
you can use

list_the_exported_thms ();;

to show a list of exported theorems together with the theory they were
exported to (i.e., the argument to logfile).

Hopefully that's the information you require.

Cheers,

Joe

On Fri, Jul 10, 2015 at 12:55 AM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
> Thanks for the reply.
>
> Yeah, such a function would be helpful
>
> Regards
> Robert
>
> On Jul 9, 2015 8:35 PM, "Joe Leslie-Hurd" <joe at gilith.com> wrote:
>>
>> Hi Robert,
>>
>> Whenever an article is generated, it is normalized so that if a type
>> or term is used multiple times then it is built once, saved in a
>> dictionary, and then pulled out when needed. For theorems this is
>> taken even further, so that theorems that are alpha-equivalent are
>> only constructed once.
>>
>> I'm afraid there's currently no infrastructure for recording which
>> article file a theorem was exported to in HOL Light. It probably
>> wouldn't be too hard to add, though, if you needed the information.
>>
>> Cheers,
>>
>> Joe
>>
>>
>> On Thu, Jul 9, 2015 at 5:12 AM, Robert White
>> <ai.robert.wangshuai at gmail.com> wrote:
>> > Dear Joe,
>> >
>> > I wonder what's behind OpenTheory when it's merging two or more article
>> > files together. Is there any optimization?
>> >
>> > By the way, for HOL Light, is there any function I can tell which thm is
>> > in
>> > which article file after exporting?
>> >
>> >
>> > Thanks a lot!
>> >
>> > --
>> >
>> > Regards,
>> > Robert White (Shuai Wang)
>> > INRIA Deducteam
>> > [Moving to ILLC of UvA from this Sep to continue my masters. ]
>> > [New email address will be shuai.wang at student.uva.nl]
>> >
>> >
>> > _______________________________________________
>> > opentheory-users mailing list
>> > opentheory-users at gilith.com
>> > http://www.gilith.com/opentheory/mailing-list
>> >
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>