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.