1\DOC new_infixr_definition 2 3\TYPE {new_infixr_definition : string * term * int -> thm} 4 5\SYNOPSIS 6Declares a new right associative infix constant and installs a 7definition in the current theory. 8 9 10 11\KEYWORDS 12definition, parsing, infix 13 14\LIBRARY 15Parse 16 17\DESCRIBE 18The function {new_infixr_definition} has exactly the same effect as 19{new_infixl_definition} except that the infix constant defined will 20associate to the right. 21 22\SEEALSO 23Definition.new_definition, Definition.new_specification, boolSyntax.new_infix, boolSyntax.new_infixl_definition. 24\ENDDOC 25