<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>Hi Rob,</div><div><br></div><div>I wanted to follow up on the HOLLight namespace issue:</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div class="im">> On this topic, I note that there are a number of names in the base package in the HOLLight namespace. E.g., "HOLLight.mk_pair. Is that intentional?</div></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div class="im">
><br>
> That is definitely not intentional, and I even have a script that ensures that no symbols in the HOLLight namespace escape to the standard theory library. I have a feeling that I have not updated the base package on gilith for too long, and will upload the latest version when I return from my vacation next week.<br>

<br>
</div> think all the names in the HOLLight namespace are related to type definitions. I look forward to seeing the updated base package.<br></blockquote><div><br></div><div>I've just updated the base package</div><div>
<br></div><div><a href="http://opentheory.gilith.com/?pkg=base">http://opentheory.gilith.com/?pkg=base</a></div><div><br></div><div>but I see that the new version also contains symbols in the HOLLight namespace.</div><div>
<br></div><div>However, the HOLLight symbol names do not appear in any exported theorem, and so are contained within a single theory package. (This is actually what my script checks, not that there are no HOLLight names anywhere.)</div>
<div><br></div><div>I believe this means is that these names are transient, and you can replace them with any fresh names (perhaps using a ProofPower version of gensym?), without changing any exported theorem in the standard theory library.</div>
<div><br></div><div>Does that resolve the issue?</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div></div></div></div>