equal
deleted
inserted
replaced
100 \item The @{text"@"} operation associates implicitly to the right, |
100 \item The @{text"@"} operation associates implicitly to the right, |
101 which leads to unpleasant line breaks if the term is too long for one |
101 which leads to unpleasant line breaks if the term is too long for one |
102 line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
102 line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
103 @{text"@"}-terms to the left before printing, which leads to better |
103 @{text"@"}-terms to the left before printing, which leads to better |
104 line breaking behaviour: |
104 line breaking behaviour: |
105 @{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>10"} |
105 @{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"} |
106 |
106 |
107 \end{itemize} |
107 \end{itemize} |
108 *} |
108 *} |
109 |
109 |
110 subsection{* Numbers *} |
110 subsection{* Numbers *} |