<div dir="ltr">Hi Rob,<div class="gmail_extra"><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">My plan was to import the base package but using the ProofPower definitions (or theorems derived from them) rather than making new definitions so that I would end up importing all the theorems about the ProofPower constants and types that I need to support the dependencies of other packages. Isn't that what you are expected to do?<br>
</blockquote><div><br></div><div>That's exactly right. In fact the construction of the base theory package is designed to help with this, in the naming of the packages that make it up. Definition theorems are stored in packages named *-def (the theorems in these packages must be derived from ProofPower theorems), and the theorems in other packages are merely consequences of these definition theorems (and can either be mapped to named ProofPower theorems or simply added to the theorem database as unnamed theorems).</div>
<div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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?<br>
</blockquote><div><br></div><div>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.</div>
<div> </div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div></div></div>