[opentheory-users] mapping names in opentheory

[Ramana Kumar]

On Mon, Jan 10, 2011 at 8:49 PM, Joe Hurd <joe at gilith.com> wrote:
>But what I would expect is that you would have functions:
>
> importName : openTheoryName -> holName
>
> exportName : holName -> openTheoryName
>
> that you would always use for converting between HOL4 names and
> OpenTheory names.

I have started adding these functions to HOL4 (the dictionaries are
there but not well-populated).
But now I am wondering about test/interpretations/hol-light.int in the
opentheory source repository.
What is the point of this file, and where/how is it used?
Is it an alternative method whereby the above functions are
unrequired, each proof assistant only ever deals with its own names
and reads/writes articles about them, and opentheory takes care of the
renaming instead?
If so, which method is preferred?