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

[Robert White]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150710/7fc467c3/attachment.html>