new_infixr_definition : string * term * int -> thm
STRUCTURE
SYNOPSIS
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.
SEEALSO
HOL  Trindemossen-1