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