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