equal
deleted
inserted
replaced
118 \item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}. |
118 \item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}. |
119 \item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n}, |
119 \item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n}, |
120 the $n$th element of \isa{xs}. |
120 the $n$th element of \isa{xs}. |
121 |
121 |
122 \item Human readers are good at converting automatically from lists to |
122 \item Human readers are good at converting automatically from lists to |
123 sets. Hence \texttt{OptionalSugar} contains syntax for supressing the |
123 sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the |
124 conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}} |
124 conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}} |
125 becomes \isa{x\ {\isasymin}\ xs}. |
125 becomes \isa{x\ {\isasymin}\ xs}. |
126 |
126 |
127 \item The \isa{{\isacharat}} operation associates implicitly to the right, |
127 \item The \isa{{\isacharat}} operation associates implicitly to the right, |
128 which leads to unpleasant line breaks if the term is too long for one |
128 which leads to unpleasant line breaks if the term is too long for one |
135 |
135 |
136 \end{itemize}% |
136 \end{itemize}% |
137 \end{isamarkuptext}% |
137 \end{isamarkuptext}% |
138 \isamarkuptrue% |
138 \isamarkuptrue% |
139 % |
139 % |
|
140 \isamarkupsubsection{Numbers% |
|
141 } |
|
142 \isamarkuptrue% |
|
143 % |
|
144 \begin{isamarkuptext}% |
|
145 Coercions between numeric types are alien to mathematicians who |
|
146 consider, for example, \isa{nat} as a subset of \isa{int}. |
|
147 \texttt{OptionalSugar} contains syntax for suppressing numeric coercions such |
|
148 as \isa{int} \isa{{\isacharcolon}{\isacharcolon}} \isa{nat\ {\isasymRightarrow}\ int}. For example, |
|
149 \isa{{\isachardoublequote}int\ {\isadigit{5}}{\isachardoublequote}} is printed as \isa{{\isadigit{5}}}. Embeddings of types |
|
150 \isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such |
|
151 as \isa{nat} \isa{{\isacharcolon}{\isacharcolon}} \isa{int\ {\isasymRightarrow}\ nat} are not and should not be |
|
152 hidden.% |
|
153 \end{isamarkuptext}% |
|
154 \isamarkuptrue% |
|
155 % |
140 \isamarkupsection{Printing theorems% |
156 \isamarkupsection{Printing theorems% |
141 } |
157 } |
142 \isamarkuptrue% |
158 \isamarkuptrue% |
143 % |
159 % |
144 \isamarkupsubsection{Question marks% |
160 \isamarkupsubsection{Question marks% |
160 reset show_question_marks; |
176 reset show_question_marks; |
161 \end{verbatim} |
177 \end{verbatim} |
162 at the beginning of your file \texttt{ROOT.ML}. |
178 at the beginning of your file \texttt{ROOT.ML}. |
163 The rest of this document is produced with this flag reset. |
179 The rest of this document is produced with this flag reset. |
164 |
180 |
165 Hint: Resetting \verb!show_question_marks! only supresses question |
181 Hint: Resetting \verb!show_question_marks! only suppresses question |
166 marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still |
182 marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still |
167 printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their |
183 printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their |
168 internal index. This can be avoided by turning the last digit into a |
184 internal index. This can be avoided by turning the last digit into a |
169 subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.% |
185 subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.% |
170 \end{isamarkuptext}% |
186 \end{isamarkuptext}% |