tat - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > tat		GIF version

Syntax Definition tat 191

Description: Indefinite descriptor.

**Assertion**
Ref	Expression
tat	term ε

This syntax is primitive. The first axiom using it is ax-wat 192.

Colors of variables: type var term