1 (*<*) |
|
2 theory Sugar |
|
3 imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" |
|
4 begin |
|
5 (*>*) |
|
6 |
|
7 section "Introduction" |
|
8 |
|
9 text{* This document is for those Isabelle users who have mastered |
|
10 the art of mixing \LaTeX\ text and Isabelle theories and never want to |
|
11 typeset a theorem by hand anymore because they have experienced the |
|
12 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}! |
|
13 and seeing Isabelle typeset it for them: |
|
14 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]} |
|
15 No typos, no omissions, no sweat. |
|
16 If you have not experienced that joy, read Chapter 4, \emph{Presenting |
|
17 Theories}, \cite{LNCS2283} first. |
|
18 |
|
19 If you have mastered the art of Isabelle's \emph{antiquotations}, |
|
20 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity |
|
21 you may be tempted to think that all readers of the stunning ps or pdf |
|
22 documents you can now produce at the drop of a hat will be struck with |
|
23 awe at the beauty unfolding in front of their eyes. Until one day you |
|
24 come across that very critical of readers known as the ``common referee''. |
|
25 He has the nasty habit of refusing to understand unfamiliar notation |
|
26 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you |
|
27 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk> |
|
28 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin |
|
29 that must be punished by instant rejection. |
|
30 |
|
31 |
|
32 This document shows you how to make Isabelle and \LaTeX\ cooperate to |
|
33 produce ordinary looking mathematics that hides the fact that it was |
|
34 typeset by a machine. You merely need to load the right files: |
|
35 \begin{itemize} |
|
36 \item Import theory \texttt{LaTeXsugar} in the header of your own |
|
37 theory. You may also want bits of \texttt{OptionalSugar}, which you can |
|
38 copy selectively into your own theory or import as a whole. Both |
|
39 theories live in \texttt{HOL/Library} and are found automatically. |
|
40 |
|
41 \item Should you need additional \LaTeX\ packages (the text will tell |
|
42 you so), you include them at the beginning of your \LaTeX\ document, |
|
43 typically in \texttt{root.tex}. For a start, you should |
|
44 \verb!\usepackage{amssymb}! --- otherwise typesetting |
|
45 @{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol |
|
46 @{text"\<nexists>"} is missing. |
|
47 \end{itemize} |
|
48 *} |
|
49 |
|
50 section{* HOL syntax*} |
|
51 |
|
52 subsection{* Logic *} |
|
53 |
|
54 text{* |
|
55 The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}. |
|
56 |
|
57 The predefined constructs @{text"if"}, @{text"let"} and |
|
58 @{text"case"} are set in sans serif font to distinguish them from |
|
59 other functions. This improves readability: |
|
60 \begin{itemize} |
|
61 \item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}. |
|
62 \item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}. |
|
63 \item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\ |
|
64 @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}. |
|
65 \end{itemize} |
|
66 *} |
|
67 |
|
68 subsection{* Sets *} |
|
69 |
|
70 text{* Although set syntax in HOL is already close to |
|
71 standard, we provide a few further improvements: |
|
72 \begin{itemize} |
|
73 \item @{term"{x. P}"} instead of @{text"{x. P}"}. |
|
74 \item @{term"{}"} instead of @{text"{}"}, where |
|
75 @{term"{}"} is also input syntax. |
|
76 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
|
77 \end{itemize} |
|
78 *} |
|
79 |
|
80 subsection{* Lists *} |
|
81 |
|
82 text{* If lists are used heavily, the following notations increase readability: |
|
83 \begin{itemize} |
|
84 \item @{term"x # xs"} instead of @{text"x # xs"}, |
|
85 where @{term"x # xs"} is also input syntax. |
|
86 If you prefer more space around the $\cdot$ you have to redefine |
|
87 \verb!\isasymcdot! in \LaTeX: |
|
88 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
|
89 |
|
90 \item @{term"length xs"} instead of @{text"length xs"}. |
|
91 \item @{term"nth xs n"} instead of @{text"nth xs n"}, |
|
92 the $n$th element of @{text xs}. |
|
93 |
|
94 \item Human readers are good at converting automatically from lists to |
|
95 sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the |
|
96 conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"} |
|
97 becomes @{prop"x \<in> set xs"}. |
|
98 |
|
99 \item The @{text"@"} operation associates implicitly to the right, |
|
100 which leads to unpleasant line breaks if the term is too long for one |
|
101 line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
|
102 @{text"@"}-terms to the left before printing, which leads to better |
|
103 line breaking behaviour: |
|
104 @{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"} |
|
105 |
|
106 \end{itemize} |
|
107 *} |
|
108 |
|
109 subsection{* Numbers *} |
|
110 |
|
111 text{* Coercions between numeric types are alien to mathematicians who |
|
112 consider, for example, @{typ nat} as a subset of @{typ int}. |
|
113 \texttt{OptionalSugar} contains syntax for suppressing numeric coercions such |
|
114 as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example, |
|
115 @{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types |
|
116 @{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such |
|
117 as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be |
|
118 hidden. *} |
|
119 |
|
120 section "Printing theorems" |
|
121 |
|
122 subsection "Question marks" |
|
123 |
|
124 text{* If you print anything, especially theorems, containing |
|
125 schematic variables they are prefixed with a question mark: |
|
126 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time |
|
127 you would rather not see the question marks. There is an attribute |
|
128 \verb!no_vars! that you can attach to the theorem that turns its |
|
129 schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}! |
|
130 results in @{thm conjI[no_vars]}. |
|
131 |
|
132 This \verb!no_vars! business can become a bit tedious. |
|
133 If you would rather never see question marks, simply put |
|
134 \begin{quote} |
|
135 @{ML "Printer.show_question_marks_default := false"}\verb!;! |
|
136 \end{quote} |
|
137 at the beginning of your file \texttt{ROOT.ML}. |
|
138 The rest of this document is produced with this flag set to \texttt{false}. |
|
139 |
|
140 Hint: Setting @{ML Printer.show_question_marks_default} to \texttt{false} only |
|
141 suppresses question marks; variables that end in digits, |
|
142 e.g. @{text"x1"}, are still printed with a trailing @{text".0"}, |
|
143 e.g. @{text"x1.0"}, their internal index. This can be avoided by |
|
144 turning the last digit into a subscript: write \verb!x\<^isub>1! and |
|
145 obtain the much nicer @{text"x\<^isub>1"}. *} |
|
146 |
|
147 (*<*)declare [[show_question_marks = false]](*>*) |
|
148 |
|
149 subsection {*Qualified names*} |
|
150 |
|
151 text{* If there are multiple declarations of the same name, Isabelle prints |
|
152 the qualified name, for example @{text "T.length"}, where @{text T} is the |
|
153 theory it is defined in, to distinguish it from the predefined @{const[source] |
|
154 "List.length"}. In case there is no danger of confusion, you can insist on |
|
155 short names (no qualifiers) by setting the \verb!names_short! |
|
156 configuration option in the context. |
|
157 *} |
|
158 |
|
159 subsection {*Variable names\label{sec:varnames}*} |
|
160 |
|
161 text{* It sometimes happens that you want to change the name of a |
|
162 variable in a theorem before printing it. This can easily be achieved |
|
163 with the help of Isabelle's instantiation attribute \texttt{where}: |
|
164 @{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of |
|
165 \begin{quote} |
|
166 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}! |
|
167 \end{quote} |
|
168 To support the ``\_''-notation for irrelevant variables |
|
169 the constant \texttt{DUMMY} has been introduced: |
|
170 @{thm fst_conv[where b = DUMMY]} is produced by |
|
171 \begin{quote} |
|
172 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
|
173 \end{quote} |
|
174 Variables that are bound by quantifiers or lambdas cannot be renamed |
|
175 like this. Instead, the attribute \texttt{rename\_abs} does the |
|
176 job. It expects a list of names or underscores, similar to the |
|
177 \texttt{of} attribute: |
|
178 \begin{quote} |
|
179 \verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}! |
|
180 \end{quote} |
|
181 produces @{thm split_paired_All[rename_abs _ l r]}. |
|
182 *} |
|
183 |
|
184 subsection "Inference rules" |
|
185 |
|
186 text{* To print theorems as inference rules you need to include Didier |
|
187 R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
|
188 for typesetting inference rules in your \LaTeX\ file. |
|
189 |
|
190 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
|
191 @{thm[mode=Rule] conjI}, even in the middle of a sentence. |
|
192 If you prefer your inference rule on a separate line, maybe with a name, |
|
193 \begin{center} |
|
194 @{thm[mode=Rule] conjI} {\sc conjI} |
|
195 \end{center} |
|
196 is produced by |
|
197 \begin{quote} |
|
198 \verb!\begin{center}!\\ |
|
199 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
|
200 \verb!\end{center}! |
|
201 \end{quote} |
|
202 It is not recommended to use the standard \texttt{display} option |
|
203 together with \texttt{Rule} because centering does not work and because |
|
204 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can |
|
205 clash. |
|
206 |
|
207 Of course you can display multiple rules in this fashion: |
|
208 \begin{quote} |
|
209 \verb!\begin{center}!\\ |
|
210 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\ |
|
211 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\ |
|
212 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\ |
|
213 \verb!\end{center}! |
|
214 \end{quote} |
|
215 yields |
|
216 \begin{center}\small |
|
217 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex] |
|
218 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad |
|
219 @{thm[mode=Rule] disjI2} {\sc disjI$_2$} |
|
220 \end{center} |
|
221 |
|
222 The \texttt{mathpartir} package copes well if there are too many |
|
223 premises for one line: |
|
224 \begin{center} |
|
225 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
|
226 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
|
227 \end{center} |
|
228 |
|
229 Limitations: 1. Premises and conclusion must each not be longer than |
|
230 the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again |
|
231 displayed with a horizontal line, which looks at least unusual. |
|
232 |
|
233 |
|
234 In case you print theorems without premises no rule will be printed by the |
|
235 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead: |
|
236 \begin{quote} |
|
237 \verb!\begin{center}!\\ |
|
238 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\ |
|
239 \verb!\end{center}! |
|
240 \end{quote} |
|
241 yields |
|
242 \begin{center} |
|
243 @{thm[mode=Axiom] refl} {\sc refl} |
|
244 \end{center} |
|
245 *} |
|
246 |
|
247 subsection "Displays and font sizes" |
|
248 |
|
249 text{* When displaying theorems with the \texttt{display} option, e.g. |
|
250 \verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is |
|
251 set in small font. It uses the \LaTeX-macro \verb!\isastyle!, |
|
252 which is also the style that regular theory text is set in, e.g. *} |
|
253 |
|
254 lemma "t = t" |
|
255 (*<*)oops(*>*) |
|
256 |
|
257 text{* \noindent Otherwise \verb!\isastyleminor! is used, |
|
258 which does not modify the font size (assuming you stick to the default |
|
259 \verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer |
|
260 normal font size throughout your text, include |
|
261 \begin{quote} |
|
262 \verb!\renewcommand{\isastyle}{\isastyleminor}! |
|
263 \end{quote} |
|
264 in \texttt{root.tex}. On the other hand, if you like the small font, |
|
265 just put \verb!\isastyle! in front of the text in question, |
|
266 e.g.\ at the start of one of the center-environments above. |
|
267 |
|
268 The advantage of the display option is that you can display a whole |
|
269 list of theorems in one go. For example, |
|
270 \verb!@!\verb!{thm[display] append.simps}! |
|
271 generates @{thm[display] append.simps} |
|
272 *} |
|
273 |
|
274 subsection "If-then" |
|
275 |
|
276 text{* If you prefer a fake ``natural language'' style you can produce |
|
277 the body of |
|
278 \newtheorem{theorem}{Theorem} |
|
279 \begin{theorem} |
|
280 @{thm[mode=IfThen] le_trans} |
|
281 \end{theorem} |
|
282 by typing |
|
283 \begin{quote} |
|
284 \verb!@!\verb!{thm[mode=IfThen] le_trans}! |
|
285 \end{quote} |
|
286 |
|
287 In order to prevent odd line breaks, the premises are put into boxes. |
|
288 At times this is too drastic: |
|
289 \begin{theorem} |
|
290 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
291 \end{theorem} |
|
292 In which case you should use \texttt{IfThenNoBox} instead of |
|
293 \texttt{IfThen}: |
|
294 \begin{theorem} |
|
295 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
296 \end{theorem} |
|
297 *} |
|
298 |
|
299 subsection{* Doing it yourself\label{sec:yourself}*} |
|
300 |
|
301 text{* If for some reason you want or need to present theorems your |
|
302 own way, you can extract the premises and the conclusion explicitly |
|
303 and combine them as you like: |
|
304 \begin{itemize} |
|
305 \item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! |
|
306 prints premise 1 of $thm$. |
|
307 \item \verb!@!\verb!{thm (concl)! $thm$\verb!}! |
|
308 prints the conclusion of $thm$. |
|
309 \end{itemize} |
|
310 For example, ``from @{thm (prem 2) conjI} and |
|
311 @{thm (prem 1) conjI} we conclude @{thm (concl) conjI}'' |
|
312 is produced by |
|
313 \begin{quote} |
|
314 \verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ |
|
315 \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! |
|
316 \end{quote} |
|
317 Thus you can rearrange or hide premises and typeset the theorem as you like. |
|
318 Styles like \verb!(prem 1)! are a general mechanism explained |
|
319 in \S\ref{sec:styles}. |
|
320 *} |
|
321 |
|
322 subsection "Patterns" |
|
323 |
|
324 text {* |
|
325 |
|
326 In \S\ref{sec:varnames} we shows how to create patterns containing |
|
327 ``@{term DUMMY}''. |
|
328 You can drive this game even further and extend the syntax of let |
|
329 bindings such that certain functions like @{term fst}, @{term hd}, |
|
330 etc.\ are printed as patterns. \texttt{OptionalSugar} provides the |
|
331 following: |
|
332 |
|
333 \begin{center} |
|
334 \begin{tabular}{l@ {~~produced by~~}l} |
|
335 @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\ |
|
336 @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\ |
|
337 @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\ |
|
338 @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\ |
|
339 @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\ |
|
340 \end{tabular} |
|
341 \end{center} |
|
342 *} |
|
343 |
|
344 section "Proofs" |
|
345 |
|
346 text {* Full proofs, even if written in beautiful Isar style, are |
|
347 likely to be too long and detailed to be included in conference |
|
348 papers, but some key lemmas might be of interest. |
|
349 It is usually easiest to put them in figures like the one in Fig.\ |
|
350 \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command: |
|
351 *} |
|
352 text_raw {* |
|
353 \begin{figure} |
|
354 \begin{center}\begin{minipage}{0.6\textwidth} |
|
355 \isastyleminor\isamarkuptrue |
|
356 *} |
|
357 lemma True |
|
358 proof - |
|
359 -- "pretty trivial" |
|
360 show True by force |
|
361 qed |
|
362 text_raw {* |
|
363 \end{minipage}\end{center} |
|
364 \caption{Example proof in a figure.}\label{fig:proof} |
|
365 \end{figure} |
|
366 *} |
|
367 text {* |
|
368 |
|
369 \begin{quote} |
|
370 \small |
|
371 \verb!text_raw {!\verb!*!\\ |
|
372 \verb! \begin{figure}!\\ |
|
373 \verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
|
374 \verb! \isastyleminor\isamarkuptrue!\\ |
|
375 \verb!*!\verb!}!\\ |
|
376 \verb!lemma True!\\ |
|
377 \verb!proof -!\\ |
|
378 \verb! -- "pretty trivial"!\\ |
|
379 \verb! show True by force!\\ |
|
380 \verb!qed!\\ |
|
381 \verb!text_raw {!\verb!*!\\ |
|
382 \verb! \end{minipage}\end{center}!\\ |
|
383 \verb! \caption{Example proof in a figure.}\label{fig:proof}!\\ |
|
384 \verb! \end{figure}!\\ |
|
385 \verb!*!\verb!}! |
|
386 \end{quote} |
|
387 |
|
388 Other theory text, e.g.\ definitions, can be put in figures, too. |
|
389 *} |
|
390 |
|
391 section {*Styles\label{sec:styles}*} |
|
392 |
|
393 text {* |
|
394 The \verb!thm! antiquotation works nicely for single theorems, but |
|
395 sets of equations as used in definitions are more difficult to |
|
396 typeset nicely: people tend to prefer aligned @{text "="} signs. |
|
397 |
|
398 To deal with such cases where it is desirable to dive into the structure |
|
399 of terms and theorems, Isabelle offers antiquotations featuring |
|
400 ``styles'': |
|
401 |
|
402 \begin{quote} |
|
403 \verb!@!\verb!{thm (style) thm}!\\ |
|
404 \verb!@!\verb!{prop (style) thm}!\\ |
|
405 \verb!@!\verb!{term (style) term}!\\ |
|
406 \verb!@!\verb!{term_type (style) term}!\\ |
|
407 \verb!@!\verb!{typeof (style) term}!\\ |
|
408 \end{quote} |
|
409 |
|
410 A ``style'' is a transformation of a term. There are predefined |
|
411 styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. |
|
412 For example, |
|
413 the output |
|
414 \begin{center} |
|
415 \begin{tabular}{l@ {~~@{text "="}~~}l} |
|
416 @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\ |
|
417 @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons} |
|
418 \end{tabular} |
|
419 \end{center} |
|
420 is produced by the following code: |
|
421 \begin{quote} |
|
422 \verb!\begin{center}!\\ |
|
423 \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
424 \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\ |
|
425 \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\ |
|
426 \verb!\end{tabular}!\\ |
|
427 \verb!\end{center}! |
|
428 \end{quote} |
|
429 Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
430 It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
431 as an antiquotation. The styles \verb!lhs! and \verb!rhs! |
|
432 extract the left hand side (or right hand side respectively) from the |
|
433 conclusion of propositions consisting of a binary operator |
|
434 (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}). |
|
435 |
|
436 Likewise, \verb!concl! may be used as a style to show just the |
|
437 conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
|
438 \begin{center} |
|
439 @{thm hd_Cons_tl} |
|
440 \end{center} |
|
441 To print just the conclusion, |
|
442 \begin{center} |
|
443 @{thm (concl) hd_Cons_tl} |
|
444 \end{center} |
|
445 type |
|
446 \begin{quote} |
|
447 \verb!\begin{center}!\\ |
|
448 \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\ |
|
449 \verb!\end{center}! |
|
450 \end{quote} |
|
451 Beware that any options must be placed \emph{before} |
|
452 the style, as in this example. |
|
453 |
|
454 Further use cases can be found in \S\ref{sec:yourself}. |
|
455 If you are not afraid of ML, you may also define your own styles. |
|
456 Have a look at module @{ML_struct Term_Style}. |
|
457 *} |
|
458 |
|
459 (*<*) |
|
460 end |
|
461 (*>*) |
|