<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">I am trying to import the base package into ProofPower from the Gilith OpenTheory Repo using my prototype OpenTheory reader. I did "opentheory install base" and that seemed to work (once I had installed the md5sha1sum package from MacPorts to resolve the dependency on sha1sum). It created a directory $HOME/.opentheory with some interesting looking things in it, in particular, a subdirectory called packages with lots of subdirectories containing, inter alia, article files.<div><br></div><div>Is the idea that I should be able to read a single article file to import an entire package? Or do I need to process the theory files somehow. Or should I not be looking in $HOME/.opentheory/packages at all but doing something else?</div><div><br></div><div>When I look at the subdirectories of $HOME/.opentheory/packages, some contain 1 article file and some contain 2. In bool-def-1.10 for example, there are 2: bool-def-1.10.art and bool-def.art. I can import the latter but not the former, because it attempts create a definition referring to a non-existent constant called bool-def-1.10. In base-1.132 there is just one article file base-1.132.art. When I try to import that I get the same kind of problem: it tries to define Data.Bool.T to be equal to a constant called base-1.132. What am I missing?</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>