[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

Ramana,

On 24 Nov 2013, at 09:45, Ramana Kumar <ramana at member.fsf.org> wrote:

> I think the idea of the base package is that everything in it should already be supported by your theorem prover, so you don't need to import it - rather, you use it as a dependency for things you export from your theorem prover.
> 
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?

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?

Regards,

Rob.