[opentheory-users] interpreting namespaces

[Ramana Kumar]

The interpret lines in a theory file enable "renaming" of specific
constants and type operators.
Would it be possible to rename an entire namespace in one go?

An example usage is extracting the lazy list theory from HOL4, which
is called llist, but in OpenTheory namespace might be better called
LazyList or Data.LazyList or something.
The automatic technology for extracting an article just uses the
theory name as the namespace by default.
I could extend the HOL4 extractor to allow a manual override.
Alternatively, I could put something in the .thy file (at the moment
it would be an "interpret" line for every constant/type operator
defined).
Which option is better?