next up previous contents
Next: Functional Programming in the Up: The Tactic Language Previous: Semantics of Other Special

Theorems with Parameters

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).

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997