next up previous contents
Next: Predeclared theorems: Up: Predeclared objects: Previous: Predeclared objects:

Predeclared objects other than built-in tactics and predeclared theorems:

true false:
Truth values.

P1 P2 Id:
The projection operators and the identity function; also their defining theorems. There are variants p1 and p2 of P1 and P2 which are used by the higher-order matching mechanism; the lower-case variants are automatically applied by the tactic interpreter where possible (as if they were functionally programmed with their defining theorems).

Equality (also a built in tactic).

Function application (also application of parameterized tactics to their arguments).

Application of unstratified ``class functions''; used for refinements of higher order matching and extension of first-order logic.

: Function composition.

Ordered pair. List constructor. Also the second component of the mixfix case expression constructor.

The first component of the mixfix case expression constructor. Not really an operator.

Randall Holmes