kct - Higher-Order Logic Explorer

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

Syntax Definition kct 10

Description: Context operator.

**Hypotheses**
Ref	Expression
ta	term A
tb	term B

**Assertion**
Ref	Expression
kct	term (A, B)

This syntax is primitive. The first axiom using it is ax-jca 17.

Colors of variables: type var term