[opentheory-users] interpreting namespaces

[Ramana Kumar]

Perhaps the "show" lines already do this?
Specifically the

show "NAMESPACE" as "NAMESPACE"

form.

Is that appropriate to use in this situation, when packaging an
article that is systematically using the wrong namespace?

On Tue, Dec 6, 2011 at 5:46 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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?