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

[Joe Leslie-Hurd]

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
>