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