src/Doc/Tutorial/Documents/Documents.thy
changeset 67398 5eb932e604a2
parent 67042 677cab7c2b85
child 67406 23307fd33906
equal deleted inserted replaced
67397:12b0c11e3d20 67398:5eb932e604a2
    42 
    42 
    43 text {*
    43 text {*
    44   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
    44   \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
    45   same expression internally.  Any curried function with at least two
    45   same expression internally.  Any curried function with at least two
    46   arguments may be given infix syntax.  For partial applications with
    46   arguments may be given infix syntax.  For partial applications with
    47   fewer than two operands, there is a notation using the prefix~@{text
    47   fewer than two operands, the operator is enclosed in parentheses.
    48   op}.  For instance, @{text xor} without arguments is represented as
    48   For instance, @{text xor} without arguments is represented as
    49   @{text "op [+]"}; together with ordinary function application, this
    49   @{text "([+])"}; together with ordinary function application, this
    50   turns @{text "xor A"} into @{text "op [+] A"}.
    50   turns @{text "xor A"} into @{text "([+]) A"}.
    51 
    51 
    52   The keyword \isakeyword{infixl} seen above specifies an
    52   The keyword \isakeyword{infixl} seen above specifies an
    53   infix operator that is nested to the \emph{left}: in iterated
    53   infix operator that is nested to the \emph{left}: in iterated
    54   applications the more complex expression appears on the left-hand
    54   applications the more complex expression appears on the left-hand
    55   side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]
    55   side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]