hb - Higher-Order Logic Explorer

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

Syntax Definition hb 3

Description: The type of booleans (true and false).

**Assertion**
Ref	Expression
hb	type ∗

This syntax is primitive. The first axiom using it is ax-cb1 29.

Colors of variables: type var term