**defineconstant**- ``defineconstant left-side right-side'', where
left-side has the correct format (an undeclared constant possibly
applied to lists of parameters) declares the new constant read from
``left-side'' and introduces a theorem with null dependencies of the
form ``left-side = right-side'', with the same name as the constant
defined.
**defineinfix**- ``defineinfix thm left-side right-side'' where
``left-side'' has a top level undeclared operator (infix or prefix)
taking as arguments and possibly applied to parameters or lists of
parameters, declares the new operator (as type level) and creates a
theorem called ``thm'' equating ``left-side'' and ``right-side''.
**definetypedinfix**- ``definetypedinfix thm left-type right-type
left-side right-side'' has the same effect as ``defineinfix thm
left-side right-side'', except that the left and right sides of the
new operator are assigned relative types ``left-side'' and
``right-side'': these arguments are numerical and are
*not*put in double quotes. **defineitconstant**- Like ``defineconstant'', except that the
right side is the current subterm.
**defineitinfix**- Like ``defineinfix'', except that the right side
is the current subterm.
**defineittypedinfix**- Like ``definetypedinfix'', except that the
right side is the current subterm.
**defineopaque**- Defines opaque operators. Same arguments as
``definetypedinfix'', except that types are not needed.

Fri Sep 5 16:28:58 MDT 1997