Theorems may have parameters; this will mean that the theorem name
will be applied using `@` to one or more lists of arguments (a
``list of arguments'' is a substitution instance of an ``argument
list'' as formally defined above) when it appears embedded. These
arguments may represent objects of the theory or other theorems or
tactics. It is possible to prove theorems whose names are operators,
in which case an instance of the theorem will have possibly left and
certainly right arguments and may further be applied to one or more
lists of additional arguments.

Parameterized theorems allow the introduction of information which is not in the target term. They demonstrate one of the two senses in which Mark2 supports a higher-order programming language (the other is explained in the following section).

Fri Sep 5 16:28:58 MDT 1997