3 \def\isabellecontext{Documents}%
6 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
10 \begin{isamarkuptext}%
11 Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure
12 for concrete syntax is that of general \bfindex{mixfix annotations}.
13 Associated with any kind of name and type declaration, mixfixes give
14 rise both to grammar productions for the parser and output templates
15 for the pretty printer.
17 In full generality, the whole affair of parser and pretty printer
18 configuration is rather subtle. Any syntax specifications given by
19 end-users need to interact properly with the existing setup of
20 Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
21 details. It is particularly important to get the precedence of new
22 syntactic constructs right, avoiding ambiguities with existing
25 \medskip Subsequently we introduce a few simple declaration forms
26 that already cover the most common situations fairly well.%
30 \isamarkupsubsection{Infix Annotations%
34 \begin{isamarkuptext}%
35 Syntax annotations may be included wherever constants are declared
36 directly or indirectly, including \isacommand{consts},
37 \isacommand{constdefs}, or \isacommand{datatype} (for the
38 constructor operations). Type-constructors may be annotated as
39 well, although this is less frequently encountered in practice
40 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
42 Infix declarations\index{infix annotations} provide a useful special
43 case of mixfixes, where users need not care about the full details
44 of priorities, nesting, spacing, etc. The subsequent example of the
45 exclusive-or operation on boolean values illustrates typical infix
49 \isacommand{constdefs}\isanewline
50 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
51 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
53 \begin{isamarkuptext}%
54 Any curried function with at least two arguments may be associated
55 with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to
56 the same expression internally. In partial applications with less
57 than two operands there is a special notation with \isa{op} prefix:
58 \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}};
59 combined with plain prefix application this turns \isa{xor\ A}
60 into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
62 \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration
63 refers to the bit of concrete syntax to represent the operator,
64 while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole
67 As it happens, Isabelle/HOL already spends many popular combinations
68 of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
69 \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
70 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
71 arrangement of inner syntax may be inspected via
72 \commdx{print\protect\_syntax}, albeit its output is enormous.
74 Operator precedence also needs some special considerations. The
75 admissible range is 0--1000. Very low or high priorities are
76 basically reserved for the meta-logic. Syntax of Isabelle/HOL
77 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
78 centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
79 HOL forms, or use the mostly unused range 100--900.
81 \medskip The keyword \isakeyword{infixl} specifies an operator that
82 is nested to the \emph{left}: in iterated applications the more
83 complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly,
84 \isakeyword{infixr} refers to nesting to the \emph{right}, reading
85 \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast,
86 a \emph{non-oriented} declaration via \isakeyword{infix} would
87 always demand explicit parentheses.
89 Many binary operations observe the associative law, so the exact
90 grouping does not matter. Nevertheless, formal statements need be
91 given in a particular format, associativity needs to be treated
92 explicitly within the logic. Exclusive-or is happens to be
93 associative, as shown below.%
96 \isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline
98 \isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
100 \begin{isamarkuptext}%
101 Such rules may be used in simplification to regroup nested
102 expressions as required. Note that the system would actually print
103 the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
104 (due to nesting to the left). We have preferred to give the fully
105 parenthesized form in the text for clarity. Only in rare situations
106 one may consider to force parentheses by use of non-oriented infix
107 syntax; equality would probably be a typical candidate.%
111 \isamarkupsubsection{Mathematical Symbols \label{sec:thy-present-symbols}%
115 \begin{isamarkuptext}%
116 Concrete syntax based on plain ASCII characters has its inherent
117 limitations. Rich mathematical notation demands a larger repertoire
118 of symbols. Several standards of extended character sets have been
119 proposed over decades, but none has become universally available so
120 far, not even Unicode\index{Unicode}.
122 Isabelle supports a generic notion of \bfindex{symbols} as the
123 smallest entities of source text, without referring to internal
124 encodings. Such ``generalized characters'' may be of one of the
125 following three kinds:
129 \item Traditional 7-bit ASCII characters.
131 \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
132 \verb,\\,\verb,<,$ident$\verb,>,).
134 \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
135 \verb,\\,\verb,<^,$ident$\verb,>,).
139 Here $ident$ may be any identifier according to the usual Isabelle
140 conventions. This results in an infinite store of symbols, whose
141 interpretation is left to further front-end tools. For example, the
142 \verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
143 $\forall$ --- both by the user-interface of Proof~General + X-Symbol
144 and the Isabelle document processor (see \S\ref{FIXME}).
146 A list of standard Isabelle symbols is given in
147 \cite[appendix~A]{isabelle-sys}. Users may introduce their own
148 interpretation of further symbols by configuring the appropriate
149 front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
150 macros for document preparation. There are also a few predefined
151 control symbols, such as \verb,\,\verb,<^sub>, and
152 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
153 (printable) symbol, respectively.
155 \medskip The following version of our \isa{xor} definition uses a
156 standard Isabelle symbol to achieve typographically pleasing output.%
161 \isacommand{constdefs}\isanewline
162 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
163 \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
166 \begin{isamarkuptext}%
167 The X-Symbol package within Proof~General provides several input
168 methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just
169 type \verb,\,\verb,<oplus>, by hand; the display is adapted
170 immediately after continuing further input.
172 \medskip A slightly more refined scheme is to provide alternative
173 syntax via the \bfindex{print mode} concept of Isabelle (see also
174 \cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
175 enabled whenever X-Symbol is active. Consider the following hybrid
176 declaration of \isa{xor}.%
181 \isacommand{constdefs}\isanewline
182 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
183 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
186 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
187 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
190 \begin{isamarkuptext}%
191 Here the \commdx{syntax} command acts like \isakeyword{consts}, but
192 without declaring a logical constant, and with an optional print
193 mode specification. Note that the type declaration given here
194 merely serves for syntactic purposes, and is not checked for
195 consistency with the real constant.
197 \medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
198 input, while output uses the nicer syntax of $xsymbols$, provided
199 that print mode is presently active. This scheme is particularly
200 useful for interactive development, with the user typing plain ASCII
201 text, but gaining improved visual feedback from the system (say in
202 current goal output).
205 Using alternative syntax declarations easily results in varying
206 versions of input sources. Isabelle provides no systematic way to
207 convert alternative expressions back and forth. Print modes only
208 affect situations where formal entities are pretty printed by the
209 Isabelle process (e.g.\ output of terms and types), but not the
210 original theory text.
213 \medskip The following variant makes the alternative \isa{{\isasymoplus}}
214 notation only available for output. Thus we may enforce input
215 sources to refer to plain ASCII only.%
218 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
219 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
221 \isamarkupsubsection{Prefix Annotations%
225 \begin{isamarkuptext}%
226 Prefix syntax annotations\index{prefix annotation} are just a very
227 degenerate of the general mixfix form \cite{isabelle-ref}, without
228 any template arguments or priorities --- just some piece of literal
231 The following example illustrates this idea idea by associating
232 common symbols with the constructors of a currency datatype.%
235 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
236 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
237 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
238 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
239 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
241 \begin{isamarkuptext}%
242 Here the degenerate mixfix annotations on the rightmost column
243 happen to consist of a single Isabelle symbol each:
244 \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
245 \verb,\,\verb,<yen>,, \verb,$,.
247 Recall that a constructor like \isa{Euro} actually is a function
248 \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
249 be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Only the head of the application is
250 subject to our concrete syntax; this simple form already achieves
251 conformance with notational standards of the European Commission.
253 \medskip Certainly, the same idea of prefix syntax also works for
254 \isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
255 might introduce a (slightly unrealistic) function to calculate an
256 abstract currency value, by cases on the datatype constructors and
257 fixed exchange rates. The funny symbol used here is that of
261 \isacommand{consts}\isanewline
262 \ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
264 \isamarkupsubsection{Syntax Translations \label{sec:def-translations}%
268 \begin{isamarkuptext}%
271 \index{syntax translations|(}%
272 \index{translations@\isacommand {translations} (command)|(}
273 Isabelle offers an additional definitional facility,
274 \textbf{syntax translations}.
275 They resemble macros: upon parsing, the defined concept is immediately
276 replaced by its definition. This effect is reversed upon printing. For example,
277 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
280 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
282 \begin{isamarkuptext}%
283 \index{$IsaEqTrans@\isasymrightleftharpoons}
285 Internally, \isa{{\isasymnoteq}} never appears.
287 In addition to \isa{{\isasymrightleftharpoons}} there are
288 \isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
289 and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
290 for uni-directional translations, which only affect
291 parsing or printing. This tutorial will not cover the details of
292 translations. We have mentioned the concept merely because it
293 crops up occasionally; a number of HOL's built-in constructs are defined
294 via translations. Translations are preferable to definitions when the new
295 concept is a trivial variation on an existing one. For example, we
296 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
297 about \isa{{\isacharequal}} still apply.%
298 \index{syntax translations|)}%
299 \index{translations@\isacommand {translations} (command)|)}%
303 \isamarkupsection{Document Preparation%
307 \begin{isamarkuptext}%
308 Isabelle/Isar is centered around a certain notion of \bfindex{formal
309 proof documents}\index{documents|bold}: ultimately the result of the
310 user's theory development efforts is a human-readable record --- as
311 a browsable PDF file or printed on paper. The overall document
312 structure follows traditional mathematical articles, with
313 sectioning, explanations, definitions, theorem statements, and
316 The Isar proof language \cite{Wenzel-PhD}, which is not covered in
317 this book, admits to write formal proof texts that are acceptable
318 both to the machine and human readers at the same time. Thus
319 marginal comments and explanations may be kept at a minimum.
320 Nevertheless, Isabelle document output is still useful without
321 actual Isar proof texts; formal specifications usually deserve their
322 own coverage in the text, while unstructured proof scripts may be
323 just ignore by readers (or intentionally suppressed from the text).
325 \medskip The Isabelle document preparation system essentially acts
326 like a formal front-end for {\LaTeX}. After checking definitions
327 and proofs the theory sources are turned into typesetting
328 instructions, so the final document is known to observe quite strong
329 ``soundness'' properties. This enables users to write authentic
330 reports on formal theory developments with little additional effort,
331 the most tedious consistency checks are handled by the system.%
335 \isamarkupsubsection{Isabelle Sessions%
339 \begin{isamarkuptext}%
340 In contrast to the highly interactive mode of the formal parts of
341 Isabelle/Isar theory development, the document preparation stage
342 essentially works in batch-mode. This revolves around the concept
343 of a \bfindex{session}, which essentially consists of a collection
344 of theory source files that contribute to a single output document.
345 Each session is derived from a parent one (usually an object-logic
346 image such as \texttt{HOL}); this results in an overall tree
347 structure of Isabelle sessions.
349 The canonical arrangement of source files of a session called
350 \texttt{MySession} is as follows:
354 \item Directory \texttt{MySession} contains the required theory
355 files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
357 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
358 for loading all wanted theories, usually just
359 \texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
360 theory dependency graph.
362 \item Directory \texttt{MySession/document} contains everything
363 required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
364 be provided initially. The latter file holds appropriate {\LaTeX}
365 code to commence a document (\verb,\documentclass, etc.), and to
366 include the generated files $A@i$\texttt{.tex} for each theory. The
367 generated file \texttt{session.tex} holds {\LaTeX} commands to
368 include \emph{all} theory output files in topologically sorted
371 \item In addition an \texttt{IsaMakefile} outside of directory
372 \texttt{MySession} holds appropriate dependencies and invocations of
373 Isabelle tools to control the batch job. The details are covered in
374 \cite{isabelle-sys}; \texttt{isatool usedir} is the most important
379 With everything put in its proper place, \texttt{isatool make}
380 should be sufficient to process the Isabelle session completely,
381 with the generated document appearing in its proper place (within
382 \verb,~/isabelle/browser_info,).
384 In practice, users may want to have \texttt{isatool mkdir} generate
385 an initial working setup without further ado. For example, an empty
386 session \texttt{MySession} derived from \texttt{HOL} may be produced
390 isatool mkdir HOL MySession
394 This runs the session with sensible default options, including
395 verbose mode to tell the user where the result will appear. The
396 above dry run should produce should produce a single page of output
397 (with a dummy title, empty table of contents etc.). Any failure at
398 that stage is likely to indicate some technical problems with your
399 {\LaTeX} installation.\footnote{Especially make sure that
400 \texttt{pdflatex} is present.}
402 \medskip Users may now start to populate the directory
403 \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
404 accordingly. \texttt{MySession/document/root.tex} should be also
405 adapted at some point; the generated version is mostly
406 self-explanatory. The default versions includes the
407 \texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for
408 mathematical symbols); further packages may required, e.g.\ for
409 unusual Isabelle symbols.
411 Realistic applications may demand additional files in
412 \texttt{MySession/document} for the {\LaTeX} stage, such as
413 \texttt{root.bib} for the bibliographic database.\footnote{Using
414 that particular name of \texttt{root.bib}, the Isabelle document
415 processor (actually \texttt{isatool document} \cite{isabelle-sys})
416 will be smart enough to invoke \texttt{bibtex} accordingly.}
418 \medskip Failure of the document preparation phase in an Isabelle
419 batch session leaves the generated sources in there target location
420 (as pointed out by the accompanied error message). In case of
421 {\LaTeX} errors, users may trace error messages at the file position
422 of the generated text.%
426 \isamarkupsubsection{Structure Markup%
430 \isamarkupsubsubsection{Sections%
434 \begin{isamarkuptext}%
435 FIXME \verb,\label, within sections;
437 The large-scale structure of Isabelle documents closely follows
438 {\LaTeX} convention, with chapters, sections, subsubsections etc.
439 The formal Isar language includes separate structure \bfindex{markup
440 commands}, which do not effect the formal content of a theory (or
441 proof), but results in corresponding {\LaTeX} elements issued to the
444 There are different markup commands for different formal contexts:
445 in header position (just before a \isakeyword{theory} command),
446 within the theory body, or within a proof. Note that the header
447 needs to be treated specially, since ordinary theory and proof
448 commands may only occur \emph{after} the initial \isakeyword{theory}
453 \begin{tabular}{llll}
454 header & theory & proof & default meaning \\\hline
455 & \commdx{chapter} & & \verb,\chapter, \\
456 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
457 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
458 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
463 From the Isabelle perspective, each markup command takes a single
464 text argument (delimited by \verb,",\dots\verb,", or
465 \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
466 surrounding white space, the argument is passed to a {\LaTeX} macro
467 \verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
468 are defined in \verb,isabelle.sty, according to the rightmost column
471 \medskip The following source fragment illustrates structure markup
472 of a theory. Note that {\LaTeX} labels may well be included inside
473 of section headings as well.
476 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
478 theory Foo_Bar = Main:
480 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
488 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
493 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
500 Users may occasionally want to change the meaning of some markup
501 commands, typically via appropriate use of \verb,\renewcommand, in
502 \texttt{root.tex}. The \verb,\isamarkupheader, is a good candidate
503 for some adaption, e.g.\ moving it up in the hierarchy to become
507 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
510 Certainly, this requires to change the default
511 \verb,\documentclass{article}, in \texttt{root.tex} to something
512 that supports the notion of chapters in the first place, e.g.\
513 \verb,\documentclass{report},.
515 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
516 hold the name of the current theory context. This is particularly
517 useful for document headings or footings, e.g.\ like this:
520 \renewcommand{\isamarkupheader}[1]%
521 {\chapter{#1}\markright{THEORY~\isabellecontext}}
524 \noindent Make sure to include something like
525 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
526 should have more than 2 pages to show the effect.%
530 \isamarkupsubsection{Formal Comments and Antiquotations%
534 \begin{isamarkuptext}%
535 Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),%
539 \isamarkupsubsection{Symbols and Characters%
543 \begin{isamarkuptext}%
544 FIXME \verb,\isabellestyle,%
548 \isamarkupsubsection{Suppressing Output%
552 \begin{isamarkuptext}%
553 By default Isabelle's document system generates a {\LaTeX} source
554 file for each theory that happens to get loaded during the session.
555 The generated \texttt{session.tex} file will include all of these in
556 order of appearance, which in turn gets included by the standard
557 \texttt{root.tex} file. Certainly one may change the order of
558 appearance or suppress unwanted theories by ignoring
559 \texttt{session.tex} and include individual files in
560 \texttt{root.tex} by hand. On the other hand, such an arrangement
561 requires additional efforts for maintenance.
563 Alternatively, one may tune the theory loading process in
564 \texttt{ROOT.ML}: traversal of the theory dependency graph may be
565 fine-tuned by adding further \verb,use_thy, invocations, although
566 topological sorting needs to be preserved. Moreover, the ML
567 operator \verb,no_document, temporarily disables document generation
568 while executing a theory loader command; the usage is like this:
571 no_document use_thy "Aux";
574 Theory output may be also suppressed \emph{partially} as well.
575 Typical applications include research papers or slides based on
576 formal developments --- these usually do not show the full formal
577 content. The special source comments
578 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
579 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the
580 document generator as open and close parenthesis for
581 \bfindex{ignored material}. Any text inside of (potentially nested)
582 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
583 parentheses is just ignored from the output --- after correct formal
586 In the following example we suppress the slightly formalistic
587 \isakeyword{theory} and \isakeyword{end} part of a theory text.
592 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
593 \texttt{theory A = Main:} \\
594 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
596 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
598 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
603 Ignoring portions of printed text like this demands some special
611 %%% TeX-master: "root"