Quelle  Documents.thy

(*<*)
theory Documents imports Main begin
(*>*)

section ‹Concrete Syntax \label{sec:concrete-syntax}›

text ‹
 The core concept of Isabelle's framework for concrete syntax is that
 of \bfindex{mixfix annotations}. Associated with any kind of
 constant declaration, mixfixes affect both the grammar productions
 for the parser and output templates for the pretty printer.

 In full generality, parser and pretty printer configuration is a
 subtle affair~cite‹"isabelle-isar-ref"›. Your syntax specifications need
 to interact properly with the existing setup of Isabelle/Pure and
 Isabelle/HOL\@. To avoid creating ambiguities with existing
 elements, it is particularly important to give new syntactic
 constructs the right precedence.

 Below we introduce a few simple syntax declaration
 forms that already cover many common situations fairly well.
 ›


subsection ‹Infix Annotations›

text ‹
 Syntax annotations may be included wherever constants are declared,
 such as \isacommand{definition} and \isacommand{primrec} --- and also
 \isacommand{datatype}, which declares constructor operations.
 Type-constructors may be annotated as well, although this is less
 frequently encountered in practice (the infix type ‹×› comes
 to mind).

 Infix declarations\index{infix annotations} provide a useful special
 case of mixfixes. The following example of the exclusive-or
 operation on boolean values illustrates typical infix declarations.
 ›

definition xor :: "bool → bool → bool"    (infixl "[+]" 60)
where "A [+] B ≡ (A ∧ ¬ B) ∨ (¬ A ∧ B)"

text ‹
 \noindent Now ‹xor A B› and ‹A [+] B› refer to the
 same expression internally. Any curried function with at least two
 arguments may be given infix syntax. For partial applications with
 fewer than two operands, the operator is enclosed in parentheses.
 For instance, ‹xor› without arguments is represented as
 ‹([+])›; together with ordinary function application, this
 turns ‹xor A› into ‹([+]) A›.

 The keyword \isakeyword{infixl} seen above specifies an
 infix operator that is nested to the \emph{left}: in iterated
 applications the more complex expression appears on the left-hand
 side, and term‹A [+] B [+] C› stands for ‹(A [+] B) [+]
 C›. Similarly, \isakeyword{infixr} means nesting to the
 \emph{right}, reading term‹A [+] B [+] C› as ‹A [+] (B
 [+] C)›. A \emph{non-oriented} declaration via \isakeyword{infix}
 would render term‹A [+] B [+] C› illegal, but demand explicit
 parentheses to indicate the intended grouping.

 The string @{text [source] "[+]"} in our annotation refers to the
 concrete syntax to represent the operator (a literal token), while
 the number ‹60› determines the precedence of the construct:
 the syntactic priorities of the arguments and result. Isabelle/HOL
 already uses up many popular combinations of ASCII symbols for its
 own use, including both ‹+› and ‹++›. Longer
 character combinations are more likely to be still available for
 user extensions, such as our~‹[+]›.

 Operator precedences have a range of 0--1000. Very low or high
 priorities are reserved for the meta-logic. HOL syntax mainly uses
 the range of 10--100: the equality infix ‹=› is centered at
 50; logical connectives (like ‹∨› and ‹∧›) are
 below 50; algebraic ones (like ‹+› and ‹*›) are
 above 50. User syntax should strive to coexist with common HOL
 forms, or use the mostly unused range 100--900.
 ›


subsection ‹Mathematical Symbols \label{sec:syntax-symbols}›

text ‹
 Concrete syntax based on ASCII characters has inherent limitations.
 Mathematical notation demands a larger repertoire of glyphs.
 Several standards of extended character sets have been proposed over
 decades, but none has become universally available so far. Isabelle
 has its own notion of \bfindex{symbols} as the smallest entities of
 source text, without referring to internal encodings. There are
 three kinds of such ``generalized characters'':

 \begin{enumerate}

 \item 7-bit ASCII characters

 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,

 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,

 \end{enumerate}

 Here $ident$ is any sequence of letters.
 This results in an infinite store of symbols, whose
 interpretation is left to further front-end tools. For example, the
 Isabelle document processor (see \S\ref{sec:document-preparation})
 display the \verb,\,\verb,∀, symbol as~‹∀›.

 A list of standard Isabelle symbols is given in
 cite‹"isabelle-isar-ref"›. You may introduce your own
 interpretation of further symbols by configuring the appropriate
 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
 few predefined control symbols, such as \verb,\,\verb,_, and
 \verb,\,\verb,^, for sub- and superscript of the subsequent
 printable symbol, respectively. For example, ▩‹A^\⋆›, is
 output as ‹A^\⋆›.

 A number of symbols are considered letters by the Isabelle lexer and
 can be used as part of identifiers. These are the greek letters
 ‹α› (\verb+\+\verb+α+), ‹β›
 (\verb+\+\verb+β+), etc. (excluding ‹λ›),
 special letters like ‹A› (\verb+\+\verb+A+) and ‹A› (\verb+\+\verb+A+). Moreover the control symbol
 \verb+\+\verb+₊ may be used to subscript a single letter or digit
 in the trailing part of an identifier. This means that the input

 \medskip
 {\small\noindent ▩‹∀α₁. α₁ = Π_\A›}

 \medskip
 \noindent is recognized as the term term‹∀α₁. α₁ = Π_\A›
 by Isabelle.

 Replacing our previous definition of ‹xor› by the
 following specifies an Isabelle symbol for the new operator:
 ›

(*<*)
hide_const xor
setup ‹Sign.add_path "version1"›
(*>*)
definition xor :: "bool → bool → bool"    (infixl "⊕" 60)
where "A ⊕ B ≡ (A ∧ ¬ B) ∨ (¬ A ∧ B)"
(*<*)
setup ‹Sign.local_path›
(*>*)

text ‹
 It is possible to provide alternative syntax forms
 through the \bfindex{print mode} concept~cite‹"isabelle-isar-ref"›. By
 convention, the mode of ``$xsymbols$'' is enabled whenever
 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
 consider the following hybrid declaration of ‹xor›:
 ›

(*<*)
hide_const xor
setup ‹Sign.add_path "version2"›
(*>*)
definition xor :: "bool → bool → bool"    (infixl "[+]🚫" 60)
where "A [+]🚫 B ≡ (A ∧ ¬ B) ∨ (¬ A ∧ B)"

notation (xsymbols) xor (infixl "⊕🚫" 60)
(*<*)
setup ‹Sign.local_path›
(*>*)

text ‹\noindent
  \commdx{notation} command associates a mixfix
  with a known constant. The print mode specification,
  ‹(xsymbols)›, is optional.

  may now write ‹A [+] B› or ‹A ⊕ B› in input, while
  uses the nicer syntax of $xsymbols$ whenever that print mode is
 . Such an arrangement is particularly useful for interactive
 , where users may type ASCII text and see mathematical
  displayed during proofs.›


subsection ‹Prefix Annotations›

text ‹
 Prefix syntax annotations\index{prefix annotation} are another form
 of mixfixes cite‹"isabelle-isar-ref"›, without any template arguments or
 priorities --- just some literal syntax. The following example
 associates common symbols with the constructors of a datatype.
 ›

datatype currency =
    Euro nat    ("euro;")
  | Pounds nat  ("£")
  | Yen nat     ("¥")
  | Dollar nat  ("$")

text ‹
 \noindent Here the mixfix annotations on the rightmost column happen
 to consist of a single Isabelle symbol each: \verb,\,\verb,euro;,,
 \verb,\,\verb,£,, \verb,\,\verb,¥,, and \verb,$,. Recall
 that a constructor like ‹Euro› actually is a function typ‹nat → currency›. The expression ‹Euro 10› will be
 printed as term‹euro; 10›; only the head of the application is
 subject to our concrete syntax. This rather simple form already
 achieves conformance with notational standards of the European
 Commission.

 Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.
 ›


subsection ‹Abbreviations \label{sec:abbreviations}›

text‹Mixfix syntax annotations merely decorate particular constant
  forms with concrete syntax, for instance replacing
 ‹xor A B› by ‹A ⊕ B›. Occasionally, the relationship
  some piece of notation and its internal form is more
 . Here we need \emph{abbreviations}.

  \commdx{abbreviation} introduces an uninterpreted notational
  as an abbreviation for a complex term. Abbreviations are
  upon parsing and re-introduced upon printing. This provides a
  mechanism for syntactic macros.

  typical use of abbreviations is to introduce relational notation for
  in a set of pairs, replacing ‹(x, y) ∈ sim› by
 ‹x ≈ y›. We assume that a constant ‹sim› of type
 typ‹('a × 'a) set› has been introduced at this point.›
(*<*)consts sim :: "('a \<times> 'a) set"(*>*)
abbreviation sim2 :: "'a → 'a → bool"   (infix "≈" 50)
where "x ≈ y ≡ (x, y) ∈ sim"

text ‹\noindent The given meta-equality is used as a rewrite rule
  parsing (replacing \mbox{prop‹x ≈ y›} by ‹(x,y) ∈
 ›) and before printing (turning ‹(x,y) ∈ sim› back into
 mbox{prop‹x ≈ y›}). The name of the dummy constant ‹sim2›
  not matter, as long as it is unique.

  common application of abbreviations is to
  variant versions of fundamental relational expressions, such
  ‹≠› for negated equalities. The following declaration
  from Isabelle/HOL itself:
 ›

abbreviation not_equal :: "'a → 'a → bool"    (infixl "~=🚫" 50)
where "x ~=🚫 y ≡ ¬ (x = y)"

notation (xsymbols) not_equal (infix "≠🚫" 50)

text ‹\noindent The notation ‹≠› is introduced separately to restrict it
  the \emph{xsymbols} mode.

  are appropriate when the defined concept is a
  variation on an existing one. But because of the automatic
  and unfolding of abbreviations, they do not scale up well to
  hierarchies of concepts. Abbreviations do not replace
 .

  are a simplified form of the general concept of
 emph{syntax translations}; even heavier transformations may be
  in ML cite‹"isabelle-isar-ref"›.
 ›


section ‹Document Preparation \label{sec:document-preparation}›

text ‹
 Isabelle/Isar is centered around the concept of \bfindex{formal
 proof documents}\index{documents|bold}. The outcome of a formal
 development effort is meant to be a human-readable record, presented
 as browsable PDF file or printed on paper. The overall document
 structure follows traditional mathematical articles, with sections,
 intermediate explanations, definitions, theorems and proofs.

 \medskip The Isabelle document preparation system essentially acts
 as a front-end to {\LaTeX}. After checking specifications and
 proofs formally, the theory sources are turned into typesetting
 instructions in a schematic manner. This lets you write authentic
 reports on theory developments with little effort: many technical
 consistency checks are handled by the system.

 Here is an example to illustrate the idea of Isabelle document
 preparation.
 ›

text_raw ‹\begin{quotation}›

text ‹
 The following datatype definition of ‹'a bintree› models
 binary trees with nodes being decorated by elements of type typ‹'a›.
 ›

datatype 'a bintree =
     Leaf | Branch 'a  "'a bintree"  "'a bintree"

text ‹
 \noindent The datatype induction rule generated here is of the form
 @{thm [indent = 1, display] bintree.induct [no_vars]}
 ›

text_raw ‹\end{quotation}›

text ‹
 \noindent The above document output has been produced as follows:

 \begin{ttbox}
 text {\ttlbrace}*
 The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
 models binary trees with nodes being decorated by elements
 of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
 *{\ttrbrace}

 datatype 'a bintree =
 Leaf | Branch 'a "'a bintree" "'a bintree"
 \end{ttbox}
 \begin{ttbox}
 text {\ttlbrace}*
 {\ttback}noindent The datatype induction rule generated here is
 of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
 *{\ttrbrace}
 \end{ttbox}\vspace{-\medskipamount}

 \noindent Here we have augmented the theory by formal comments
 (using \isakeyword{text} blocks), the informal parts may again refer
 to formal entities by means of ``antiquotations'' (such as
 \texttt{\at}\verb,{text "'a bintree"}, or
 \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
 ›


subsection ‹Isabelle Sessions›

text ‹
 In contrast to the highly interactive mode of Isabelle/Isar theory
 development, the document preparation stage essentially works in
 batch-mode. An Isabelle \bfindex{session} consists of a collection
 of source files that may contribute to an output document. Each
 session is derived from a single parent, usually an object-logic
 image like \texttt{HOL}. This results in an overall tree structure,
 which is reflected by the output location in the file system
 (the root directory is determined by the Isabelle settings variable
 \verb,ISABELLE_BROWSER_INFO,).

 \medskip The easiest way to manage Isabelle sessions is via
 \texttt{isabelle mkroot} (to generate an initial session source
 setup) and \texttt{isabelle build} (to run sessions as specified in
 the corresponding \texttt{ROOT} file). These Isabelle tools are
 described in further detail in the \emph{Isabelle System Manual}
 cite‹"isabelle-system"›.

 For example, a new session \texttt{MySession} (with document
 preparation) may be produced as follows:

 begin{verbatim}
 isabelle mkroot MySession
 isabelle build -D MySession
 end{verbatim}

 The \texttt{isabelle build} job also informs about the file-system
 location of the ultimate results. The above dry run should be able
 to produce some \texttt{document.pdf} (with dummy title, empty table
 of contents etc.). Any failure at this stage usually indicates
 technical problems of the {\LaTeX} installation.

 \medskip The detailed arrangement of the session sources is as
 follows.

 \begin{itemize}

 \item Directory \texttt{MySession} holds the required theory files
 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.

 \item File \texttt{MySession/ROOT} specifies the session options and
 content, with declarations for all wanted theories; it is sufficient
 to specify the terminal nodes of the theory dependency graph.

 \item Directory \texttt{MySession/document} contains everything
 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
 provided initially.

 The latter file holds appropriate {\LaTeX} code to commence a
 document (\verb,\documentclass, etc.), and to include the generated
 files $T@i$\texttt{.tex} for each theory. Isabelle will generate a
 file \texttt{session.tex} holding {\LaTeX} commands to include all
 generated theory output files in topologically sorted order, so
 \verb,\input{session}, in the body of \texttt{root.tex} does the job
 in most situations.

 \end{itemize}

 One may now start to populate the directory \texttt{MySession} and
 its \texttt{ROOT} file accordingly. The file
 \texttt{MySession/document/root.tex} should also be adapted at some
 point; the default version is mostly self-explanatory. Note that
 \verb,\isabellestyle, enables fine-tuning of the general appearance
 of characters and mathematical symbols (see also
 \S\ref{sec:doc-prep-symbols}).

 Especially observe the included {\LaTeX} packages \texttt{isabelle}
 (mandatory), \texttt{isabellesym} (required for mathematical
 symbols), and the final \texttt{pdfsetup} (provides sane defaults
 for \texttt{hyperref}, including URL markup). All three are
 distributed with Isabelle. Further packages may be required in
 particular applications, say for unusual mathematical symbols.

 \medskip Any additional files for the {\LaTeX} stage go into the
 \texttt{MySession/document} directory as well. In particular,
 adding a file named \texttt{root.bib} causes an automatic run of
 \texttt{bibtex} to process a bibliographic database; see also
 \texttt{isabelle document} cite‹"isabelle-system"›.

 \medskip Any failure of the document preparation phase in an
 Isabelle batch session leaves the generated sources in their target
 location, identified by the accompanying error message. This lets
 you trace {\LaTeX} problems with the generated files at hand.
 ›


subsection ‹Structure Markup›

text ‹
 The large-scale structure of Isabelle documents follows existing
 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
 The Isar language includes separate \bfindex{markup commands}, which
 do not affect the formal meaning of a theory (or proof), but result
 in corresponding {\LaTeX} elements.

 From the Isabelle perspective, each markup command takes a single
 $text$ argument (delimited by \verb,",~‹…›~\verb,", or
 \verb,{,\verb,*,~‹…›~\verb,*,\verb,},). After stripping any
 surrounding white space, the argument is passed to a {\LaTeX} macro
 \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are
 defined in \verb,isabelle.sty, according to the meaning given in the
 rightmost column above.

 \medskip The following source fragment illustrates structure markup
 of a theory. Note that {\LaTeX} labels may be included inside of
 section headings as well.

 \begin{ttbox}
 section {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}

 theory Foo_Bar
 imports Main
 begin

 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}

 definition foo :: \dots

 definition bar :: \dots

 subsection {\ttlbrace}* Derived rules *{\ttrbrace}

 lemma fooI: \dots
 lemma fooE: \dots

 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}

 theorem main: \dots

 end
 \end{ttbox}
 ›


subsection ‹Formal Comments and Antiquotations \label{sec:doc-prep-text}›

text ‹
 Isabelle \bfindex{source comments}, which are of the form
 \verb,(,\verb,*,~‹…›~\verb,*,\verb,),, essentially act like
 white space and do not really contribute to the content. They
 mainly serve technical purposes to mark certain oddities in the raw
 input text. In contrast, \bfindex{formal comments} are portions of
 text that are associated with formal Isabelle/Isar commands
 (\bfindex{marginal comments}), or as standalone paragraphs within a
 theory or proof context (\bfindex{text blocks}).

 \medskip Marginal comments are part of each command's concrete
 syntax cite‹"isabelle-isar-ref"›; the common form is ``\verb,--,~$text$''
 where $text$ is delimited by \verb,",‹…›\verb,", or
 \verb,{,\verb,*,~‹…›~\verb,*,\verb,}, as before. Multiple
 marginal comments may be given at the same time. Here is a simple
 example:
 ›

lemma "A --> A"
  ― ‹a triviality of propositional logic›
  ― ‹(should not really bother)›
  by (rule impI) ― ‹implicit assumption step involved here›

text ‹
 \noindent The above output has been produced as follows:

 begin{verbatim}
 lemma "A --> A"
 -- "a triviality of propositional logic"
 -- "(should not really bother)"
 by (rule impI) -- "implicit assumption step involved here"
 end{verbatim}

 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
 command, associated with the macro \verb,\isamarkupcmt, (taking a
 single argument).

 \medskip Text blocks are introduced by the commands \bfindex{text}
 and \bfindex{txt}. Each takes again a single $text$ argument,
 which is interpreted as a free-form paragraph in {\LaTeX}
 (surrounded by some additional vertical space). The typesetting
 may be changed by redefining the {\LaTeX} environments of
 \verb,isamarkuptext, or \verb,isamarkuptxt,, respectively
 (via \verb,\renewenvironment,).

 \medskip The $text$ part of Isabelle markup commands essentially
 inserts \emph{quoted material} into a formal text, mainly for
 instruction of the reader. An \bfindex{antiquotation} is again a
 formal object embedded into such an informal portion. The
 interpretation of antiquotations is limited to some well-formedness
 checks, with the result being pretty printed to the resulting
 document. Quoted text blocks together with antiquotations provide
 an attractive means of referring to formal entities, with good
 confidence in getting the technical details right (especially syntax
 and types).

 The general syntax of antiquotations is as follows:
 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
 for a comma-separated list of options consisting of a $name$ or
 \texttt{$name$=$value$} each. The syntax of $arguments$ depends on
 the kind of antiquotation, it generally follows the same conventions
 for types, terms, or theorems as in the formal part of a theory.

 \medskip This sentence demonstrates quotations and antiquotations:
 term‹%x y. x› is a well-typed term.

 \medskip\noindent The output above was produced as follows:
 \begin{ttbox}
  {\ttlbrace}*
 This sentence demonstrates quotations and antiquotations:
 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
 {\ttrbrace}
 \end{ttbox}\vspace{-\medskipamount}

 The notational change from the ASCII character~\verb,%, to the
 symbol~‹λ› reveals that Isabelle printed this term, after
 parsing and type-checking. Document preparation enables symbolic
 output by default.

 \medskip The next example includes an option to show the type of all
 variables. The antiquotation
 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
 output @{term [show_types] "%x y. x"}. Type inference has figured
 out the most general typings in the present theory context. Terms
 may acquire different typings due to constraints imposed by their
 environment; within a proof, for example, variables are given the
 same types as they have in the main goal statement.

 \medskip Several further kinds of antiquotations and options are
 available cite‹"isabelle-isar-ref"›. Here are a few commonly used
 combinations:

 \medskip

 \begin{tabular}{ll}
 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
 \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
 \end{tabular}

 \medskip

 Note that \attrdx{no_vars} given above is \emph{not} an
 antiquotation option, but an attribute of the theorem argument given
 here. This might be useful with a diagnostic command like
 \isakeyword{thm}, too.

 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
 particularly interesting. Embedding uninterpreted text within an
 informal body might appear useless at first sight. Here the key
 virtue is that the string $s$ is processed as Isabelle output,
 interpreting Isabelle symbols appropriately.

 For example, \texttt{\at}\verb,{text "∀∃"}, produces ‹∀∃›, according to the standard interpretation of these symbol
 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
 mathematical notation in both the formal and informal parts of the
 document very easily, independently of the term language of
 Isabelle. Manual {\LaTeX} code would leave more control over the
 typesetting, but is also slightly more tedious.
 ›


subsection ‹Interpretation of Symbols \label{sec:doc-prep-symbols}›

text ‹
 As has been pointed out before (\S\ref{sec:syntax-symbols}),
 Isabelle symbols are the smallest syntactic entities --- a
 straightforward generalization of ASCII characters. While Isabelle
 does not impose any interpretation of the infinite collection of
 named symbols, {\LaTeX} documents use canonical glyphs for certain
 standard symbols cite‹"isabelle-isar-ref"›.

 The {\LaTeX} code produced from Isabelle text follows a simple
 scheme. You can tune the final appearance by redefining certain
 macros, say in \texttt{root.tex} of the document.

 \begin{enumerate}

 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
 \texttt{a\dots z} are output directly, digits are passed as an
 argument to the \verb,\isadigit, macro, other characters are
 replaced by specifically named macros of the form
 \verb,\isacharXYZ,.

 \item Named symbols: \verb,\,\verb,🚫, is turned into
 \verb,{\isasymXYZ},; note the additional braces.

 \item Named control symbols: \verb,\,\verb,🚫, is turned into
 \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
 control macro is defined accordingly.

 \end{enumerate}

 You may occasionally wish to give new {\LaTeX} interpretations of
 named symbols. This merely requires an appropriate definition of
 \verb,\isasymXYZ,, for \verb,\,\verb,🚫, (see
 \texttt{isabelle.sty} for working examples). Control symbols are
 slightly more difficult to get right, though.

 \medskip The \verb,\isabellestyle, macro provides a high-level
 interface to tune the general appearance of individual symbols. For
 example, \verb,\isabellestyle{it}, uses the italics text style to
 mimic the general appearance of the {\LaTeX} math mode; double
 quotes are not printed at all. The resulting quality of typesetting
 is quite good, so this should be the default style for work that
 gets distributed to a broader audience.
 ›


subsection ‹Suppressing Output \label{sec:doc-prep-suppress}›

text ‹
 By default, Isabelle's document system generates a {\LaTeX} file for
 each theory that gets loaded while running the session. The
 generated \texttt{session.tex} will include all of these in order of
 appearance, which in turn gets included by the standard
 \texttt{root.tex}. Certainly one may change the order or suppress
 unwanted theories by ignoring \texttt{session.tex} and load
 individual files directly in \texttt{root.tex}. On the other hand,
 such an arrangement requires additional maintenance whenever the
 collection of theories changes.

 Alternatively, one may tune the theory loading process in
 \texttt{ROOT} itself: some sequential order of \textbf{theories}
 sections may enforce a certain traversal of the dependency graph,
 although this could degrade parallel processing. The nodes of each
 sub-graph that is specified here are presented in some topological
 order of their formal dependencies.

 Moreover, the system build option \verb,document=false, allows to
 disable document generation for some theories. Its usage in the
 session \texttt{ROOT} is like this:

 begin{verbatim}
 theories [document = false] T
 end{verbatim}

 \medskip Theory output may be suppressed more selectively, either
 via \bfindex{tagged command regions} or \bfindex{ignored material}.

 Tagged command regions works by annotating commands with named tags,
 which correspond to certain {\LaTeX} markup that tells how to treat
 particular parts of a document when doing the actual type-setting.
 By default, certain Isabelle/Isar commands are implicitly marked up
 using the predefined tags ``\emph{theory}'' (for theory begin and
 end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
 commands involving ML code). Users may add their own tags using the
 \verb,%,\emph{tag} notation right after a command name. In the
 subsequent example we hide a particularly irrelevant proof:
 ›

lemma "x = x" by %invisible (simp)

text ‹
 The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
 Tags observe the structure of proofs; adjacent commands with the
 same tag are joined into a single region. The Isabelle document
 preparation system allows the user to specify how to interpret a
 tagged region, in order to keep, drop, or fold the corresponding
 parts of the document. See the \emph{Isabelle System Manual}
 cite‹"isabelle-system"› for further details, especially on
 \texttt{isabelle build} and \texttt{isabelle document}.

 Ignored material is specified by delimiting the original formal
 source with special source comments
 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
 \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped
 before the type-setting phase, without affecting the formal checking
 of the theory, of course. For example, we may hide parts of a proof
 that seem unfit for general public inspection. The following
 ``fully automatic'' proof is actually a fake:
 ›

lemma "x ≠ (0::int) ==> 0 < x * x"
  by (auto(*<*)simp add: zero_less_mult_iff(*>*))

text ‹
 \noindent The real source of the proof has been as follows:

 begin{verbatim}
  by (auto(*<*)simp add: zero_less_mult_iff(*>*))
\end{verbatim}
%(*

  \medskip Suppressing portions of printed text demands care.  You
  should not misrepresent the underlying theory development.  It is
  easy to invalidate the visible text by hiding references to
  questionable axioms, for example.
\<close>

(*<*)
end
(*>*)