new_infixr_definition
boolSyntax.new_infixr_definition : string * term * int -> thm
Declares a new right associative infix constant and installs a definition in the current theory.
The function new_infixr_definition has exactly the same effect as
new_infixl_definition except that the infix constant defined will
associate to the right.
See also
Definition.new_definition,
Definition.new_specification,
boolSyntax.new_infix,
boolSyntax.new_infixl_definition