The theory environment consists of the constant and operator declaration list, the master theorem list, and some satellite declaration lists and lists containing syntactical information. A theory has a name which associates it with a file.

**Precedences:**- A list of operator precedences. Parity of the
precedence determines left/right associativity (even gives right,
odd left). Default precedence of all operators is 0.
**Default left arguments:**- A list of default left arguments for
unary operators.
**Declarations:**- There is a list of declarations of constants,
operators, and free variable operators (the last only for relative
typing purposes; free variable operators which do not need to be
typed do not need to be declared).
**Opacity declarations:**- A list of operators declared opaque.
**Pretheorems:**- A list of names of theorems which are intended to
be proved; needed to make recursive tactics possible while
preserving declaration checking for embedded theorems.
**Definitions:**- A list of constants and operators with the
theorems which define them; the name of the theorem will be the same
as the name of the defined object, if it is a constant.
**Functional programs:**- A list of automatic bindings of theorems
to constants and operators, implementing functional programming in
the tactic language.
**Theorems:**- There is a list of theorems; this also includes
images of current and old saved proof environments. The structure
of an individual theorem parallels the structure of a proof
environment as noted above, with the addition of the list of
theorems supporting the module system. Proof environments saved on
the theorem list lose ``position of selected subterm'' information,
since this is the one item in the structure of a proof environment
that is not found in a theorem.

Fri Sep 5 16:28:58 MDT 1997