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

Syntax Definition kbr 9
Description: Infix operator.
Ref Expression
ta term A
tb term B
tf term F
Ref Expression
kbr term [AFB]

This syntax is primitive. The first axiom using it is ax-wov 71.

Colors of variables: type var term
  Copyright terms: Public domain W3C validator