A `view` is an interpretation of a subset of a source theory in a
target theory, implemented as a set of translations of names of
constants and operators. Views reside in the source theory; they are
saved in theory files.

Views are constructed using the `declareview` command, which
creates a trivial view with the predeclared constants and operators
interpreted as themselves. They can be edited using the `
viewasin`, `viewasselfin`, and `dropfromview` commands.

Views are used to export theorems from the theory in which they reside
(the source theory) to another theory (the target theory). The target
theory needs to be saved on the desktop. The theorem export functions
`exportthmlist` and `exportthm`, given a view, information
about default prefixes to add to automatically generated names of
constants and operators, a single theorem or list of theorems to be
exported, and a target theory, will retrieve the target theory from
the desktop, automatically check the validity of the view and extend
it if necessary (the view must at lest include interpretations of all
axioms and definitions on which the exported theorems depend, and
often does not need to include more than this; the rest can usually be
deduced), and generate analogous theorems in the target theory,
guaranteed to be valid theorems of the target theory. The facility
will automatically avoid name conflicts by adding additional prefixes
to automatically generated names. If a tactic is exported, it will
automatically determine what other theorems need to be exported and
translate them as well; complex mutually recursive systems of tactics
can be exported reliably. A reason to extend views beyond the minimal
level of axioms and definitions is to avoid the copying of frequently
used theorems found in many theories.

The theorem export commands can be finicky about defined notions in the source theory; these need to match defined notions in the target theory with analogous definitions. The redefinition facilities might be useful in avoiding problems with this.

The theorem export commands do not export module structure; they will export modules but they are unpacked completely.

Fri Sep 5 16:28:58 MDT 1997