Declares a new right associative infix constant and installs a
definition in the current theory.
LIBRARY
Parse
DESCRIPTION
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.