The predeclared operators which implement the tactic language are the rule infixes =>, <=, =>> and <<=. There are additional related operators *>, <* and !! which will be explained below. The operators @ and , of function application and pairing have special roles in the tactic language as well. The predeclared operator = can be used as a theorem constructor. There are special unary ``delay'' operators # and ## explained below.
There are also predeclared mathematical operators +!, *!, -!, /!, %!, <!, and =! of unlimited precision unsigned integer arithmetic which are executed by the tactic interpreter.
A new predeclared operator : implements type labels as retractions onto ``strongly Cantorian sets''.