Initial work towards an OpenTheory reader for inner HOL

Currently missing some of the derived rules, and all the definitional
rules. (Also, needs testing!) Also, will require a name map to be built,
and functions for looking up things in the inner thy.

The plan is initially not to support articles that make definitions.
Have to think about the design if we want to support definitions.