[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

Hi Rob,

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?
>

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).

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?
>

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.

Cheers,

Joe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131203/6d85738f/attachment.html>