equal
deleted
inserted
replaced
141 \end{center} |
141 \end{center} |
142 |
142 |
143 |
143 |
144 |
144 |
145 \item Functions and value bindings cannot be defined inside antiquotations; they need |
145 \item Functions and value bindings cannot be defined inside antiquotations; they need |
146 to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
146 to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} |
147 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
147 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
148 the Cookbook, however, ensures that the environment markers are not printed. |
148 the Cookbook, however, ensures that the environment markers are not printed. |
149 |
149 |
150 \item Line numbers can be printed using |
150 \item Line numbers can be printed using |
151 \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} |
151 \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"} |
152 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
152 for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs. |
153 |
153 |
154 \end{itemize} |
154 \end{itemize} |
155 |
155 |
156 *} |
156 *} |